The Research Of CTL-based Model Repair

With the wide application of computer systems,the society which is highly informationized has higher requirements for the correctness and security of systems.Formal verification technology stands out among many verification methods by virtue of its ability to analyze and verify complex systems effectively.Formal verification analyze and verify the software and hardware systems of the computer through mathematical expressions,so as to ensure the security and reliability of the system.As a research field of formal verification,model checking has attracted wide attention due to its high degree of automation.The basic idea of model checking is to traverse the finite state space of the model through modeling and analyzing the computer system,and then judge whether the system satisfies the property specification which is given to be tested.When the model is judged to violate the properties,the model checking algorithm will feedback the failure information and require inspectors to debug and repair the model manually,which will sharply decrease work efficiency.Therefore,there is great meaning and value in studying an efficient automatic model repair method.This paper mainly studies CTL model verification and model repair.The main work is as follows:1.In this paper,we first study the label algorithm of classic CTL model checking.According to the CTL formula checking process,we propose the spanning tree theory of model checking with some properties of graph algorithm.We discuss and analyze the generation structure of the model after the execution of the label algorithm,and then we obtain the correlation property between the test algorithm and spanning tree,at the same time,the corresponding theoretical proof is given.2.We study the fixed point repair problem of Kripke structure,and then extend the model check problem based on the fixed point to model repair.We discuss the property of fixed point in classical model checking,and then the fixed point theory is applied to the process of model repair,we design the fixed point repair algorithm of CTL formula,meanwhile,the algorithm complexity analysis and correctness proof are also provided.Finally,we give an example to perform the application of fixed point repair in practice.3.On the basis of minimal-change model repair,the state-preserving model repair algorithm with polynomial time complexity is proposed to preserve as much useful information as possible in the original model.If the model is checked to violate the given property,we can find out the failure paths in the model by the fixed point idea of classical model checking and then repair them.In addition,since global model repair is proven to be NP-hard,the scope constraint of the repair algorithm is discussed in a subset of CTL.According to the idea of minimal model repair,we consider two kinds of repair operations which have the least influence on the states in the original model.At the same time,based on the classical model checking,the fixed point idea and some properties of the graph algorithm are combined to construct the State-Preserving model repair algorithm of the corresponding logical formulas.Finally,an example is given to illustrate the value of the algorithm in practical application.