Abstract model checking: Difference between revisions

Revision as of 19:18, 26 January 2007

Revision as of 19:30, 26 January 2007

Line 1:

{{Uncategorized|January 2007}}

{{categorize}}

'''Abstraction Model checking''' is for systems where an actual representation is too complex and and a state space explosion will result in developing the model alone. So, the design undergoes a kind of translation to scaled down "abstract" version. <br />

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.

Line 19:

==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--1542}}

[[Category:Formal methods]]