Research Of Model Checking Technique Based On Modal Logic

Modal logic is one of the most important branches of Logic.Especially,the establishment of Kripke Possible World let modal logic have a accurate and reliable semantic model,which promotes the rapid development of modal logic.Model checking technique is an important part of formal verification.It can automatically verify the correctness of both software systems and hardware systems,and thus has drawn great attention in software engineering and industry.However,state space explosion,system properties description and long counterexample understanding are three main challenges of model checking.In order to ensure the reliability and security of large and complex systems,how to effectively apply modal logic to model checking to improve the ability of model checking is a significant work,and meanwhile,it is also an important topic in theoretical computer science and software engineering fields.Focus on this topic,the paper mainly studies the following aspects:(1)A state space reduction method about finite state transition system is proposed.The method chooses proper final coalgebra of endofunctor,and generates the minimum finite state transition system using the bisimulation equivalence in modal logic theory.The transition system can completely equally simulate all the behavior of original transition system,ensure verification equivalence and effectively avoid state space explosion.(2)A class of abstract CTL formula templates under Global scope to correctly describe system properties are constucted.First,study system properties and behavior in order to prove the feasibility and necessity of formally describing the pattern and scope parameters using composite proposition.Then,through the studies about LTL and CTL,the paper presents an approach to describe system properties using CTL.At the same time,redefining three logic operators makes CTL formula templates simplified and easy to understand.Finally,the paper constructs all the CTL formula templates under Global scope in order to generate the CTL formula for describing system properties and behavior defined by composite proposition class,pattern and scope.Aim at the CTL formula templates constructed,the paper presents the correctness proof of the templates,thus proves the CTL formula templates can generate correct CTL formula.(3)It also constructs abstract CTL formula templates under Before scope to describe system properties correctly.First,through the studies about the grammar and semantic of FIL,the paper presents the shortness of FIL in describing system properties and behavior.Especially in the representation of the result described by Prospec,CTL has an irreplaceable advantage,besides,CTL is the input language of many excellent model checkers.Then,with the further study about commonly used system behavior,the abstract CTL formula templates are extended to receive composite proposition as parameters,which makes CTL template construction complete.After that,the paper proves that the CTL templates constructed can correctly generate CTL formula that describes system properties and behavior,and the description is brief and effective.These templates can be applied in existing model checkers using CTL as input language,and act as system properties description tools.At last,the paper gives the instance of CTL formula templates constructed.(4)An algorithm for deriving minimum unsatisfiable subformula with weight-based bipartite graph evolution is proposed,for deriving approximate minimum unsatisfiable subformula.First,the paper presents the definition of bipartite graph evolution and weight-based bipartite graph evolution.Then,the paper analyzes the relationship among maximum satisfiable subformula and minimum unsatisfiable subformula and smallest minimum unsatisfiable subformula,and gives the relation theorem.Finally,through the mathematic model of weight-based bipartite graph evolution,the paper presents the approach for deriving approximate minimum unsatisfiable subformula,and presents the correctness proof.The algorithm automatically generate the subclause collection of minimum unsatisfiable subformula,and derive approximate minimum unsatisfiable subformula fast and accurately.Thus get rid of irrelevant variables in counterexamples as many as possible,and improve the efficiency of error locating.