Study Of Some Key Issues On Model Checking In Formal Analysis

Model Checking is one of the most successful automatic verification techniques in the past two decades.Because of its high level automation and high efficiency, model checking has been widely used in the analysis and verification of concurrent system.One of its major advantages in comparison to such methods as theorem proving is the production of a counterexample,which explains how the system violates some assertion.However,it is a tedious task to understand the complex counterexamples generated by model checker.At the same time,we also need to spend lots of time to check out thousands of evens and signals before discover the real bug.These objective factors directly affect the efficiency of model checking verification.Therefore,how to automatically extract useful information to aid the understanding of counterexample is an area of active research.Therefore,the paper mainly analyzes minimization of counterexamples,soloves state explosion and extends Promela three aspects on Model Checking,which contents are as follows:First,introduces the main ideas of the algorithm Gastin.P proposes,and then gives an informal analysis on the well-known NS public-key authentication protocol,whose result demonstrates it is very effective,finally proposes a new algorithm-framework combining with syntax reordering strategy,solving the shortcoming that the algorithm has to revisited some states already visited in the course of searching the minimal counterexample.Second,studies from four aspects,such as atomicity,reducing the range of random variables,syntax reordering and partial order reduction to solve the state explosion of model checking.Theories'analysis and experiments'result illustrate these strategies are able to effectively reduce the number of states.Third,extends stack and queue data structures based on basic data structure in Promela,mainly defining and achieving the sequence stack and cycle queue.