Back to Search
Start Over
Temporal Logic Query Checking: A Tool for Model Exploration.
- Source :
- IEEE Transactions on Software Engineering; Oct2003, Vol. 29 Issue 10, p898-914, 17p, 1 Black and White Photograph, 4 Diagrams, 8 Charts
- Publication Year :
- 2003
-
Abstract
- Temporal logic query checking was first introduced by W. Chan in order to speed up design understanding by discovering properties not known a priori. A query is a temporal logic formula containing a special symbol ?<subscript>1</subscript>, known as a placeholder. Given a Kripke structure and a propositional formula δ, we say that δ satisfies the query if replacing the placeholder by δ results in a temporal logic formula satisfied by the Kripke structure. A solution to a temporal logic query on a Kripke structure is the set of all propositional formulas that satisfy the query. Query checking helps discover temporal properties of a system and, as such, is a useful tool for model exploration. In this paper, we show that query checking is applicable to a variety of model exploration tasks, ranging from invariant computation to test case generation. We illustrate these using a Cruise Control System. Additionally, we show that query checking is an instance of a multi-valued model checking of Chechik et al. This approach enables us to build an implementation of a temporal logic query checker, TLQSolver, on top of our existing multi-valued model checker χChek. It also allows us to decide a large class of queries and introduce witnesses for temporal logic queries--an essential notion for effective model exploration. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 00985589
- Volume :
- 29
- Issue :
- 10
- Database :
- Complementary Index
- Journal :
- IEEE Transactions on Software Engineering
- Publication Type :
- Academic Journal
- Accession number :
- 12657673
- Full Text :
- https://doi.org/10.1109/TSE.2003.1237171