Research Of Symbol Model Checking

As the computer hardware and software systems become more and more complex,testing and simulation can not assured the correctness and reliability of many such systems.In the 1980s,a formal verification technique,model checking,was proposed independently by Clarke and Emerson in the United States and by Quielle and Sifakis in France.In this formal approach, system speifications are expressed in a propositional.temporal logic,and finite-state reactive systems(circuit designs and protocols)are modeled as state-transition systems.An efficient search procedure is used to determine if the specification is true of the transition system. However,when the size of the transition systems increases and the number of global system states may grow exponentially,the state explosion that is a main disadvantage of model checking occurs.In 1986,Bryant improved the technique about binary decision diagram BDD to get reduced ordered binary decision diagram ROBDD that is a kind of boolean function canonical form.Afterwards,McMillan used BDD in model checking,and this model checking based on BDD is called Symbolic Model Checking.The main characteristic of Symbolic Model Checking is that sets about states and state-transitions of finite-state reactive system are expressed implicitly by BDD,and it relieves effectively the state explosion.Here we have realized a Symbolic Model Checker,named CTLMC(Computed-Tree Model Checker).This model checker uses Boolean function as the formal language descripting system models and CTL(Computed-Tree Logic)as the formal language descripting system properties that should be satisfied,and uses the symbolic model checking algorithm to determine whether the model satisfy properties.Furthermore,in the during of realizing the CTLMC,an improved algorithm of PRE(?) operation in Symbolic Model Checking based on OBDD is discovered,and it traverses OBDD B((?)plr....(?)pnr.B is a step in PRE(?)operation),and "deletes" all the nodes whose variables (plr,...,pnr)are quantified,and gets a non-deterministic OBDD NB that equals(?)plr....(?)pnr.B, which then is translated into an OBDD B(?)plr....(?)pnr.The result shows that it can effectively reduce the time and space of PRE(?)operation.