Constructing and Reasoning about Abstractions and Refinements
Project members:
Shiva Nejati, Arie Gurfinkel, Marsha Chechik
Description
Most realistic artifacts are too large to verify directly and
need to be abstracted. Such abstractions should be constructed
so that verification of the abstracted system allows us to say something
about correctness of the original system.
Classical abstraction is sound only with respect to universally-quantified
properties, e.g., if an invariant holds on an abstract system, it holds
on the concrete one. If a reachability property holds on an
abstract system, it is not clear whether it holds on the original one.
If a universally-quantified property fails to hold, one can use
counter-example based abstraction refinement to make
the abstraction more precise so as to avoid the spurious counter-example.
3-valued abstraction preserves truth and falsity of arbitrary temporal logic
properties. Of course, it is possible that the verification engine
determines that the answer to the property is Maybe, at which point
the verification is inconclusive and the abstraction needs to be
refined.
There are many ways to compute 3-valued abstractions. One of them
comes from abstract interpretation of programs, where a predicate p
is determined to be True if it is true in the concretization of the
system, False if it is false in the concretization, and Maybe if
its value in the concrete system cannot be determined.
Current and Future Projects in This Area
- Abstract interpretation. Our previous work, reported
in ISF and in Wei Ding's M.Sc. thesis, has started our interest in
multi-valued modeling and reasoning, but a lot more work needs
to be done here. Looking for students.
- 3-Valued SPIN. SPIN is a state-of-the-art model-checker.
Our goal is to create a version of SPIN that can analyze three-valued
models. The work on this project has started, and is related to
finite-path semantics for LTL and many other projects we do.
- Stuttering Refinement. Over the past year, Shiva Nejati
has been working on a type of refinement for
three-valued models that allows one abstract state to be repeated
(a finite number of times) and preserves a large class of temporal
logic properties. Shiva also has an algorithm for determining
whether two models are stutter refinements of each other.
This work is her M.Sc. thesis, and a paper written in collaboration
with Arie Gurfinkel and myself is currently being finished.
- 3-valued Counter-Example Based Abstraction Refinement
The idea here is to build a framework using counter-examples for
those properties that resulted in Maybe answers to refine abstractions.
We are also interested in comparing this framework with the classical
in order to quantify effectiveness of 3-valued abstraction. Looking
for students to join Arie Gurfinkel and myself on this project.
- From Classical to 3-valued AbstractionOne can reduce 3-valued model-checking to two questions to
the classical model-checker. This should allow reuse of a lot of
ideas associated with reasoning about classical abstractions,
in particular, assume/guarantee reasoning. We are interested
in investigating such parallels and looking for students to join in.
- We are also very interested in case studies that use 3-valued
abstractions.
Most relevant publications and related work:
Classical abstraction and refinement
- Clarke, Grumberg, Jha, Lu, Veith.
Counterexample-guided
abstraction refinement. In Proceedings of CAV'00.
- There are several excellent surveys and talks on this area:
- Orna Grumberg, Abstractions and Reductions in Model Checking,
In NATO Science Series, Vol. 62, 2001, Marktoberdorf summer school.
- David Schmidt. Proving
Properties about Abstractions and Refinements, Bell Labs, Naperville,
IL, Feb. 2000 (it is a talk)
- David Schmidt [Talk].
Binary
relations for abstraction and refinement (17 November). Technical
Report 2000-3. Corrected version of the paper in Proc. Workshop on Refinement
and Abstraction, Amagasaaki, Japan, Nov. 1999, Elsevier Electronic
Notes in Theoretical Computer Science
- Yannis Kassios's presentation of some of these
results as part of a
course project in csc 2108
- D. Dams, R. Gerth, O. Grumberg, Abstract Interpretation of Reactive Systems,
ACM Transactions on Programming Languages and Systems (TOPLAS), 1997.
3-valued Abstraction and Refinement
- M. Chechik, W. Ding, Lightweight Reasoning about Program Correctness,
Information Systems Frontiers, 2002.
- S. Shoham, O. Grumberg. A Game-Based Framework for CTL Counter-Examples and 3-Valued Abstraction-Refinement, CAV'03.
- Shiva Nejati, Refinement Relations on Partial Specifications,
M.Sc. thesis, University of Toronto, 2003.
- P. Godefroid, R. Jagadeesan, Automatic Abstraction Using Generalized
Model Checking, in CAV'02
Classical and 3-valued model-checking
-
M. Chechik, B. Devereux, A. Gurfinkel. Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN, in SPIN'01 Workshop on
Model-Checking Software.
- G.J. Holzmann, "The Model Checker SPIN", IEEE Transactions on Software
Engineering, 279-295, Vol. 23, No. 5, May 1997
- G. Bruns, P. Godefroid, Model Checking Partial State Spaces with 3-Valued Temporal Logics, CAV'99.
- G. Bruns, P. Godefroid, Generalized Model Checking: Reasoning about
Partial State Spaces, CONCUR'00.
Last updated: Sept. 3, 2003