AbstractionIn Model[[computer science]] and in [[mathematics]], '''abstraction model checking ''' is a form of [[model checking]] 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 />▼{{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 [[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==
The real and the abstract state spaces are galois[[Galois connection|Galois connected]]. whichThis 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. <br />
That is,
<math>\eta</math>(<math>\theta</math>(abstract)) = abstract <br/>
<math>\theta</math>(<math>\eta</math>(real)) <math>\supsetsupseteq</math> real
==See also==
==Abstraction refinement loop==
{{cmn|
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- <br/>
* [[Abstract interpretation]]
1. Obtain the abstract model <br/>
* [[Automated theorem proving]]
2. Model check and see if everything is ok. <br/>
* [[Computation tree logic]]
3. If there is a counter example, then go back to the real state space and find out if it actually a counter model. <br/>
* [[Formal verification]]
4. If not, return and continue model checking. <br/>
* [[List of model checking tools]]
* [[Program analysis (computer science)]]
* [[Static code analysis]]
}}
==References==
{{Reflist}}
* {{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=19921994| volume=16 | issue=5 | pages=1512--15421512–1542 | doi=10.1145/186025.186051| citeseerx=10.1.1.79.3022 | s2cid=207884170 }}
[[Category:Model checking]]
| 