Abstract model checking: Difference between revisions

Revision as of 17:31, 4 October 2009

Revision as of 09:49, 15 September 2010

Line 2:

'''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 [[Variable (mathematics)|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.

==Galois connected==

Line 22:

==References==

* {{cite journal | author=Edmund M. Clarke and Orna Grumberg and David E. Long | title=Model checking and abstraction | journal=ACM Transactions on Programming Languages and Systems| year=1992| volume=16 | issue=5 | pages=1512--15421512–1542 | doi=10.1145/186025.186051}}

[[Category:Formal methods]]