Composition Abstraction Spin Model Checking Based On Promela And Its Application

Model Checking is an important formal verification technique which can automatically check whether the system is holding the desired properties or not.Model Checking has been successfully applied in the analysis and verification of computer hardware,communication protocols,control systems and safety certification,etc.Since it exhaustively searches the state space,for concurrent systems,state space grows exponentially with the number of concurrent components,resulting in the state space explosion problem.Composition and abstraction methods can abstract the system into a finite state model.It can remove the irrelevant details of the properties to verify, using as little states as possible to describe the states of system.Therefore,it,to some extent,reduces the complexity of Model Checking,and thus relieves the state space explosion problem.In this dissertation,we propose a framework of combination and abstraction,give theoretical analysis,and point out the scope of a framework for adaptation.We extend combination and abstraction methods,by establishing agents Kripke structure,then compose the abstract Kripke structure based on LTL properties,and finally verify the properties with Spin model checker to reduce the number of states.Through analyzing Promela model characteristics in details and checking the Promela model of the protocol by Spin,we introduce methods to reduce the complexity of Model Checking.The results showed that combination and abstraction framework can effectively relieve the state explosion problem,the approach of using atomic and reducing the number of proctype process can reduce the complexity of Model Checking.Based on the work above,we demonstrate the approaches by taking NSPK protocol as an example.We establish a Promela model of NSPK,verify the LTL properties by Spin and analyze the results.Then,we point out the flaws of NSPK protocol and also analyze the modified NSPK.For the protocol with multiple agents,we establish the Kripke structure,apply composition and abstraction methods,and then compare the number of states between the original models and the abstracted models,showing that the framework is feasible.In the Model Checking of ATM UML models,we transform the UML models into Promela model,under the condition of preserving the checking properties,establishing the abstract Promela model by the framework.The results further show the practicality of the composition and abstraction framework.