Theory And Methodology Of Model Checking MSVL Programs Based On Dynamic Symbolic Execution

Software is an indispensable part in the national defense construction, the national economy and the people's livelihood. How to improve the correctness, reliability and security of software systems is a great challenge in computer science. Model checking proposed by Clarke is considered by far the most promising approach to deal with this challenge. Model checking has been successfully used in the verification of the software systems, but there are still some problems to be solved such as the difficulty in abstracting system models, limitation of the expressive power of the property description language, different notations are used to specify programs and properties of programs, as well as the state space explosion problem.With this motivation, the model checking approach and the dynamic symbolic execution technology are studied. A new model checking approach is given where the dynamic symbolic execution technology is applied to the model checking approach. The three main contributions of this thesis are outlined as follows.1. The syntactic structures, basic semantics as well as normal form theories of Modeling, Simulation and Verification Language(MSVL) and Propositional Projection Temporal Logic(PPTL) are studied. The theory and method of model checking MSVL programs based on dynamic symbolic execution are proposed to solve the four existing problems in model checking area. First of all, the symbolic execution tree which can be obtained by the dynamic symbolic execution of an MSVL program is viewed as a program model. This method avoids the difficulty in abstracting system models. Next, PPTL is used to specify the property to be verified which will overcome the limitation of the expressive power of the property description language because of the full-regular expressiveness of PPTL. Then, MSVL and PPTL are both the subsets of Projection Temporal Logic(PTL), the model and the property are both in the same logic system which will avoid additional conversion works and improve the efficiency of verification. Finally, the symbolic execution tree which can be obtained by the dynamic symbolic execution of an MSVL program is an abstract model, a path in this abstract model represents all the execution paths that satisfy the path constraints. This abstract method can dramatically reduce the states in the program model, thus the state space explosion problem is alleviated to a certain extent.2. Based on the original MSVL interpreter, the basic framework of MSVL programs model checker based on dynamic symbolic execution is designed. The design and realization scheme of the three main modules in the model checker is given and the model checker is then implemented by C++.3. Two examples are provided to demonstrate the correctness and availability of the model checker developed. One of them is “air condition controller”, the other is “automatic door control system”.