Design and analysis of systems using model checking and Petri net.

摘要

Model checking is one of the formal verification techniques used to verify the correctness of a finite state concurrent system. In this approach, an exhaustive search over the state-space of the concurrent system is done to determine the truth of specifications for the system expressed in temporal logic. The popularity of model checking has increased because the method is fast and automatic. Unlike other techniques, model checking produces a counter example when a fault in the system design exists. This automatic generation of a counter example can be used to pinpoint a bug in the design. A limitation exists in the way the resources are used, because in concurrent systems the number of states grows exponentially and as the number of processes increase there is a need for more memory spaces. This phenomenon is known as the state explosion problem. One of the approaches for handling a state explosion problem is to represent sets of states instead of individual states. This representation can be done using an efficient data structure, called ordered binary decision diagrams ( OBDDs). Such a model checking technique is known as symbolic model checking. In OBDD, variable ordering plays the crucial role in verification time. The verification task is automated by the use of tools like the Symbolic Model Verifier ( SMV).;Besides, the model checker, a modeling tool like Petri net can be used for system verification. Petri net can be extended as the mathematical tool so that the behavior of the system can be expressed in terms of algebraic equations and use the proof system, such as Grobner proof system, to validate the system design.;In this thesis, we verified two different system designs, Automated Guided Vehicle (AGV) and traffic light, for correctness by using the SMV model checker. We performed reachability analysis on their Petri net by using Grobner basis. The effect of various variable orders in OBDD is explored in the AGV problem.