Simulation Based Model Checking  Posted on:20080717  Degree:Doctor  Type:Dissertation  Country:China  Candidate:Z B Yuan  Full Text:PDF  GTID:1118360272466933  Subject:Computer software and theory  Abstract/Summary:  PDF Full Text Request  Formal verification is a process in which mathematical techniques are used to guarantee the correctness of a design with respect to some specified behavior. Automated formalverification tools based on modelchecking technology, have enjoyed a substantial and growing use over the last few years, showing an ability to discover subtle ?aws that result fromextremely improbable events. It is fair to say that automated verification is one of the mostsuccessful applications of automated reasoning in computer science.The automata theoretic approach offers a uniform algorithmic framework for modelchecking linear time properties. The standard approach to linear temporal logic modelchecking consists of translating the negation of a given linear temporal logic formula intoa BÃ¼chi automaton, and checking the product of the property automaton and the model oflanguage emptiness. The quality of the translation affects the resources required by themodel checking experiment. This motivates the search for algorithms that generate efficientautomata, i.e.. automata with few states, few transitions ,and simple acceptance conditions.An automaton A can replace another automaton A in model checking if A and A accept the same language. Since checking language equivalence is in general hard, practicalapproaches resort to various notions of simulations that account for the acceptance conditions of the automata. Simulation is a stronger notion than language containment becausethe simulating automaton cannot look ahead the moves of the simulated one. On the otherhand, several variants of simulation relations can be computed in polynomial time; amongthem, direct simulation, fair simulation, and delayed simulation. Ksimulation, where 1simulation corresponds to ordinary simulation and its variants for BÃ¼chi automata, and Ksimulations, for K > 1, generalize the game definition of 1simulation by allowing theprotagonist to use K pebbles instead of 1 (to"hedge its bets") in response to the antagonist's move of a single pebble.Based Ksimulation we can get more potential reduction in automaton size. We are suggesting an approximate minimization algorithm for BÃ¼chiautomata based on Ksimulation.Translation of linear temporal logic to BÃ¼chi automata results naturally in generalizedBÃ¼chi automata,that is, BÃ¼chi automata with multiple acceptance sets. A generalized BÃ¼chiautomaton with l acceptance conditions and n states can be easily converted to a simpleBÃ¼chi automaton with nl states (and one acceptance condition). Thus, it is extremely important to be able to further minimize generalized BÃ¼chi automata without first convertingthem to simple BÃ¼chi automata. As a result we are suggesting an approximate minimizationalgorithm for direct/fair/delayed simulation.The left and right languages belong to the automata theoretic part of the reduction problem. The left (resp. right) language is the set of calculations leading to (resp. starting from)a state. Ksimulations enable a fast detection of these trace inclusions. we are suggestingan approximate minimization algorithm for Kripke structure, BÃ¼chi and generalized BÃ¼chiautomata based on left and right languages.An obvious method for trying to avoid the state explosion problem is to use the natural decomposition of the system. The goal is verify properties of individual components,infer that these hold in the complete system, and use them to deduce additional properties of the system. When verifying properties of the components, it may also be necessaryto make assumption about the environment. This is approach is exemplified by Pnueli'sassumeguarantee paradigm. The real bottleneck of this framework is checking for simulation between models, thus replacing the exists simulation by the fair simulation reduces thiscomplexity to polynomial and eliminates the bottleneck of the framework.In spite of the impressive progress in the development of model checking, it is stilllimited in their ability to handle large systems. It is generally recognized that abstractiontechniques are one of the most general state reduction techniques. A novel efficient algorithm for computing abstraction of Kripke structure based on Ksimulation is proposed. Thesoundness and completeness of abstraction framework in Linear temporal logic are proved.
 Keywords/Search Tags:  model checking, simulation, Büchi automata, generalized Büchi automata, game, left right language, composition verification, abstraction  PDF Full Text Request  Related items 
 
