Research On LTL Property Decomposition Based On SPIN

In the modern world, software empowers all kinds of electronic infrastructure from the simplest TV remote controller to the most sophisticated satellite. Any slightest error or bug in the code may lead to unthinkable disaster. Therefore, several methods have been developed for producing reliable software. Formal method, including model checking, is one of them.Model checking is a technique for automatically verifying correctness properties of finite state systems, it is usually quite fast and can provide counterexamples if the design contains an error. However, the main challenge in model checking is dealing with the state space explosion problem. Currently, simplifying the complex model effectively to facilitate the checking process has become one of the vital research topics in the field. This thesis focuses on mitigating state space explosion problem in model checking, mainly involving the decomposition of linear temporal logic (LTL) properties as well as the simplification of the model being checked.The main contributions of this thesis are illustrated as follows.(1)The main theories and key technologies of model checking are summarized, including the main principles and concepts, LTL and CTL checking algorithms, typical tools and their applications. Then based on the above, the main challenge of model checking, i.e. the state space explosion problem, is pointed out, and the general solutions are summarized.(2) A well-known model checking tool SPIN is introduced and analyzed, including its ways of working, model construction process based on the Promela language, the corresponding search algorithms. Then several examples for model checking by using SPIN are demonstrated. Furthermore, this thesis explores and discusses the main approaches to tackling the state space explosion in SPIN, including partial order reduction and on-the-fly, which lays a foundation for the following approach proposed in this dissertation.(3) An approach to reducing the state space explosion based on the LTL property decomposition and program slicing is proposed. For different combinations of the logic and temporal operators, the property decomposition patterns are discussed, then programs are sliced according to the slice criteria constructed from each sub property, and the simplified models are checked by SPIN. Consequently, the verification of the original model is replaced by the verification of sub models with respect to their corresponding sub properties. It can run automatically and combine with the existing partial order reduction method to further reduce the state space explosion.(4)Based on the above approach, a prototype system is designed and implemented with the FeaVer tool and Frama-C slice plug-in. According to the experiments on some selected programs, it can effectively mitigate the state space explosion and make the checking of the correctness properties be realized successfully.