Abstraction model checking


Abstraction model checking

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.

Galois connected

The real and the abstract state spaces are Galois connected. This 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,

eta( heta(abstract)) = abstract heta(eta(real)) supset real

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.

References

*


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Model Checking — Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d origine informatique ou électronique). Il s agit de vérifier algorithmiquement si un modèle donné, le système lui même ou une… …   Wikipédia en Français

  • Model checking — This article is about checking of models in computer science. For the checking of models in statistics, see regression model validation. In computer science, model checking refers to the following problem: Given a model of a system, test… …   Wikipedia

  • Model checking — Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d origine informatique ou électronique). Il s agit de vérifier algorithmiquement si un modèle donné, le système lui même ou une… …   Wikipédia en Français

  • Model-based testing — is the application of Model based design for designing and optionally executing the necessary artifacts to perform software testing. Models can be used to represent the desired behavior of the System Under Test (SUT), or to represent the desired… …   Wikipedia

  • Abstraction (computer science) — In computer science, abstraction is the process by which data and programs are defined with a representation similar to its pictorial meaning as rooted in the more complex realm of human life and language with their higher need of summarization… …   Wikipedia

  • Model View ViewModel — The Model View ViewModel (MVVM) is an architectural pattern used in software engineering that originated from Microsoft as a specialization of the Presentation Model design pattern introduced by Martin Fowler.[1] Largely based on the Model view… …   Wikipedia

  • PAT (model checker) — PAT Developer(s) National University of Singapore Initial release 2008 (2008) Stable release 3.4(Beta) / August 27, 2011; 2 months ago (2011 08 27 …   Wikipedia

  • BLAST model checker — The Berkeley Lazy Abstraction Software Verification Tool (BLAST) is a software model checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated… …   Wikipedia

  • Formal equivalence checking — process is a part of electronic design automation (EDA), commonly used during the development of digital integrated circuits, to formally prove that two representations of a circuit design exhibit exactly the same behavior. Equivalence checking… …   Wikipedia

  • Economic model — A diagram of the IS/LM model In economics, a model is a theoretical construct that represents economic processes by a set of variables and a set of logical and/or quantitative relationships between them. The economic model is a simplified… …   Wikipedia


We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.