Research On Lazy Slicing-based Model Checking

The rapid development of Information Technology makes various computer hardwareand software have infiltrated into every corner of social production and life. Computerhardware and software systems are profoundly affecting and changing the operating modelof human society. Computer information systems are more and more important in thedevelopment of human society. However, when people are enjoying the efficiency andconvenience of information systems, they are also taking risks in the failure of hardwareand software systems. How to ensure the correctness and reliability of the hardware andsoftware systems has become a serious problem faced by the aerospace, military, economicand other aspects. The complexity of software is presenting the trend of exponential growthcaused by the integration of various systems and the emergence of concurrent systems.Therefore, the correctness verification of complex hardware and software systems hasbecome an important and challenging topic.As an important formal verification method, model checking can build precise modelsof large-scale systems for reasoning and verification. At present, more and more researchersbegin to pay attention to software model checking. The state space explosion problem ismore serious in software model checking. Moreover, infinite data structure and controlstructure common in software systems also make the state space of software system modelsoften be infinite, which is the biggest challenge faced by software model checking. Assoftware systems is becoming more and more intelligent, how to build a precise model foran intelligent reasoning system has gradually become a new problem of model checking. Inaddition, how to understand a large scale counter-example automatically and efficiently hasbecome a new obstacle to the application of model checking in software verification.Therefore, study further on the model checking theory and its application softwareverification has high theoretical and practical values.The following work has been carried out in this thesis in order to meet the challenge insoftware model checking.1) A modeling method based on small fix point computation is proposed to buildConditional Transition System for production knowledge base in model checking. Thismethod first defines the constructor function of the state set of Conditional Transition System, then proves the existence of the fix point and the small fix point of CTS constructorfunction. Furthermore, it also proves the state set S is the small fix point of its constructorfunction. Finally it gives a solving method of the state set of CTS, so that the model of CTScan be built by solving the small fixed point of constructor function of state set. Thismethod can greatly improve the efficiency of production knowledge base modeling andfault diagnosis.2) A state space exploration method based on lazy slicing is proposed. This method canrefines only a local state space that is not explored before guided by dead end state bytaking the feasible equivalent state of the feasible prefix of spurious counterexample asinitial state. Cover relation makes this method be able to validate a given property using thework has been done previously, which avoids the repeated computation caused byCEGAR-based slicing method. The counterexample with ascending precisions makesspurious counterexample decision can be done by concretizing only the last path fragmentother than the whole path, thus the cost of concretizing the path fragments before the lastpath fragment is reduced. Moreover, lazy slicing preserves the guard conditions with regardto the precision of the current over-approximate slicing in order to keep the completeness ofthe guards of events, which makes lazy slicing be able to build a more preciseover-approximate slicing.3) Two extended algorithms of lazy slicing are proposed. The first one is lazy slicingbased LTL model checking algorithm which makes lazy slicing be able to verify LTLproperty. It first computes the product of the over-approximate slicing of the original modeland the negative nondeterministic Büchi automata, then performs lazy slicing on thisproduct automata. This method enhances the verification ability of lazy slicing as well asthe reduction ability of LTL model checking. Moreover, an state space reduction algorithmbased on the orthogonalization between lazy slicing and abstract is proposed to compressthe abstract state space, which make lazy slicing be able to deal with infinite state spacewith the help of abstract. This method also makes model checker scale to large scale statespace.4) An counterexample understanding method is proposed to explain thecounterexample of model checking. This method first computes the weakest precondition ofthe counterexample from the last state on by event rule and assignment rule, then computethe inconsistent proof between the weakest precondition and the initial state by SAT solver, finally, it parses the Craig interpolation which is responsible for the failure ofcounterexample from the inconsistent proof. This computation process can be done in lineartime which improves the efficiency of counterexample understanding significantly.