Research On Formal Verification-based Parameterized Protocols

With the rapid development of computer technology,network technology and electronic information technology in all walks of life,the multi-processor system and multi-core architecture become more and more popular in the architecture of computer systems,and its validity and reliability become more and more prominent.Parameterized protocols are widely used in the multi-core structure of computer system,and the verification of the parameterized protocols has become the key in the design process as the complexity of system design increases.A subtle mistake can make serious trouble.Therefore,the verification of parameterized protocols has become a research hot spot in international academic and industrial.The formal verification uses symbol to describe the behavior and property of the parameterized protocols,and verifies it by various mathematical logic algorithms.Formal verification with advantages in completeness and high coverage has become an important method in parameterized protocols verification.In the field of parameterized protocols verification,there are many formal verification methods,but each method has some disadvantages,such as theorem proving needs manual intervention and has a low automation degree,and the main drawback of model checking is the state space explosion.These all limit the effectiveness of formal verification of parameterized protocols.This paper makes a classification and deep analysis on existing methods of formal verification of parameterized protocols,and then solves the problem from two sides,which are increasing the level of automation of theorem prover and relieving the state space explosion problem of model checking.This paper proposes two verification methods and proves the effectiveness on MESI,MutualEx,GERMAN,FLASH and other typical parameterized protocols.The main research results of this paper are as follows:(1)This paper presents a verification method based on inductive invariants and flow analysis.The method analyzes the causal relationship between the invariants and rules of parameterized protocols,and finds inductive invariants automatically by search algorithm of inductive invariants,these invariants facilitate scripts generation using the theorem prover.In addition,this paper introduces the flow analysis,and analyzes the content of the parameterized protocols during the pre-verification phase,and further analyzes and verifies the correctness of parameterized protocols.The paper gives the overall framework and implementation to the method,and conducts experiments on a variety of parameterized protocols which demonstrates the effectiveness of the proposed approach.(2)This paper presents a verification method based on predicate abstraction by CVC4 solver.The method applies predicate abstraction to the Murphi model checking,and finds the abstract states corresponding to concrete states by using CVC4 solver.The method solves the problem of state space explosion of model checking as the size of system scale increases,and the result of experiment is encouraging.