Abstraction model checking

From Wikipedia, the free encyclopedia

The introduction to this article provides insufficient context for those unfamiliar with the subject matter.
Please help improve the introduction to meet Wikipedia's layout standards. You can discuss the issue on the talk page.

This article (or section) may need to be wikified to meet Wikipedia's quality standards.
Please help improve this article, especially its section layout, and relevant internal links. (help)
This article has been tagged since February 2007.

Abstraction Model checking is for systems where an actual representation is too complex in developing the model alone. So, the design undergoes a kind of translation to scaled down "abstract" version.

The set of variables are partitioned into visible and invisible depending on their change of values. The real state space is summarized into a smaller set of the visible ones.

[edit] Galois connected

The real and the abstract state spaces are galois connected which means that if we take an element from the abstract space, concretize it and abstract the concretized version, the result will be equal to the original. On the other hand, if you pick an element from the real space, abstract it and concretize the abstract version, the final result will be a super set of the original.

That is,

$η$ ( $θ$ (abstract)) = abstract
$θ$ ( $η$ (real)) $\supset$ real

[edit] Abstraction refinement loop

A problem with abstraction model checking is that although the abstraction simulates the real, when the abstraction does not satisfy a property, it does not mean that this property actually fails in the real model. Counter examples are checked against the real state space because we obtain "spurious" counter examples. So a part of the abstraction refinement loop is:

Obtain the abstract model
Model check and see if everything is ok.
If there is a counter example, then go back to the real state space and find out if it actually a counter model.
If not, return and continue model checking.

Spurious examples are mostly generated because dead end states and bad states are abstracted to the same kind. To solve this we need to create a segregation between the 2 kinds. The next step is to find the subset of invisible variables that actually make a difference between the dead end and bad states and add this subset to the set of visible or monitored variables. If the separation proves expensive, refinement could be based on learning from samples.

[edit] References

Edmund M. Clarke and Orna Grumberg and David E. Long (1992). "Model checking and abstraction". ACM Transactions on Programming Languages and Systems 16 (5): 1512--1542.

Retrieved from "http://en.wikipedia.org../../../a/b/s/Abstraction_model_checking.html"