Model Exploration with Model-Checking

Project members:

Description:

The first of these approaches is query-checking. A query is a temporal logic formula containing a special symbol ?, known as a placeholder. Given a Kripke structure and a propositional formula p, we say that p satisfies the query if replacing the placeholder by p 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. Thus, query-checking helps discover temporal properties that hold in the system.

Query-checking is also useful for a variety of software engineering applications, such as guided simulation, testcase generation. Some of these applications have been describe in our TSE'03 paper. We are currently interested in exploring further applications of this work. See future work for some of the projects.

to hold, and as such considered to be the most useful form of output from model-checkers. Reported explanations are typically short and described in terms of states and transitions of the model; as a result, they can be effectively used for debugging. However, counter-examples are not available for every CTL property and are often inadequate for explaining exactly what the answer means. Proof-like counter-examples, an approach we recently developed, allows us to produce a proof why the property holds. This proof can then be converted into counter-examples or witnesses, for the ease of visualization. Further, it facilitates understanding and navigation through the counter-example. We are currently working on several extensions of this work (see below).
 
 

Most relevant publications

• A. Gurfinkel, M. Chechik, B. Devereux. Temporal Logic Query Checking: A Tool for Model Exploration, to appear in Transactions on Software Engineering, 2003. This paper describes query-checking and some of its applications.
• A. Gurfinkel, M. Chechik. Proof-Like Counter-Examples, TACAS'03. This paper describes proof-like counterexamples and discusses how these can be used to navigate to interesting parts of the counter-example.
• M. Chechik. How Model-Checking Can Help Model Understanding. A talk on this subject.

Tools:

Future work:

• query checking partial systems: Currently, only classical systems can be query checked. Yet, an increasing fraction of systems are partial which is often represented using three-valued logic. The goal of the project is to enable querying such models.
• query-checking with proof-like counter-examples Given that we can produce proofs as evidence why a property holds or fails to hold, can such proofs be queried for further information?
• vacuity checking Consider a property "always (not(3=5) implies p)". This property holds vacuously, i.e., there are no states that satisfy the expression not(3=5). The problem of finding instances of vacuous properties has been addressed in several recent papers. We are using query-checking to help detect instances of vacuity. A paper on this subject is forthcoming.
• use of proof-like counter-examples to help debug systems: The idea here is to use model-checker-generated evidence, in form of proofs, to help the user, automatically or semi-automatically, to trace the evidence to the source of the real bug. Ideas are welcome!
• LTL query-checking: Many of query-checking applications we've explored require that the query is formulated in LTL. Currently, our model-checker XChek only uses CTL. The goal of this project is augment XChek with handling LTL and augmenting the query-checker to use it.
• Applications:
  • Exploration case study: we would like to study usefulness of our model-exploration approaches on a real case study.
  • Test case generation using query-checking: in our TSE'03 paper we showed that one can formulate a test coverage criterium as a temporal logic query and then use the resulting witnesses as testcases. Moreover, we think this approach can work for a variety of functional coverage criteria. In this project we would like to check our hypothesis and apply the resulting strategies to generating testcases for realistic systems.
  • Finding mode confusion: We are currently applying query-checking to help understand mode confusion in avionics software. Looking for students to join us.
  • Goal refinement: Query-checking is useful to fill in the missing pieces when refining a goal into subgoals, e.g., during some requirements engineering processes. We are currently exploring this direction.