Software Reliability Verification Method Based On Model Checking

With the rapid development of information technology, the application fields of software systems are continously expanding, making their functions as well as scales become more and more complicated. Failures occurred in these softwares will cause immeasurable loss. How to effectively guarantee the reliability of software systems becomes a very urgent and serious problem. As an important formal verification technique, model cheking has been gradually used in software reliability verification. This work studies software reliability validation method based on model checking technology, and tries to solve the difficulty in complex software modeling and state space explosion.Firstly, model checking is applied into software design stage. A software design modeling method based on state transition matrix (STM) is proposed, and its formal definition and dynamic behavior is explained in details. Time and probability factors are introduced into STM models in order to solve complex software system modeling problems. Based on the extended Time STM model, we present the detailed symbolic encoeding and property description methods for real-time software design verification, and verify its satisfiability of design specifications by bounded model cheking. The experimental results prove the effectiveness of the method in software design of reliability verification.Then, model checking is applied into code development stage. A program backone based software source code abstraction method is proposed, which also helps to accelerate property verification.Through code pruning and circular path compression, we present a program backbone extraction method from software source code. Furtherly, we adopt Hoare Logic to compute an invariant for circular node to replace the complex circular path, which can greatly shorten the length of path encoding formula, and reduce the state space explosion problem to a certain extent. Finally, experimental results show that the method based on program backbone can substantially improve the efficiency of software source code reliability validation.