Guided Model Checking of Petri Nets

OData support
Supervisor:
Molnár Vince
Department of Measurement and Information Systems

Model checking is a formal verification technique for verifying requirements on behavioral models of systems in a mathematically precise way. An advantage of model checking is that in case the requirements are violated, it can produce an execution trace (counterexample) to demonstrate the incorrect behavior of the system. When analyzing state reachability, it is especially important to generate traces to reachable states, because a lot of applications (e.g., model-based testing) use them as the primary output of the model checker.

Traditional model checking algorithms systematically and often exhaustively explore the state-space of the system, i.e., they build the graph representation of the state-space. These algorithms are called explicit model checkers, because they explicitly enumerate the states and state transitions of the system. While explicit approaches are mature, they are inherently limited by the size of the state-space that can fit into memory. Unfortunately, even relatively small systems can have huge state-spaces, a phenomenon that is commonly referred to as state-space explosion.

One reason of state-space explosion in concurrent systems is the interleaving semantics of model checking, i.e., total ordering of independent, asynchronous operations. Examination of each interleaving leads to a large amount of intermediate states that are irrelevant with regard to the requirements. The main idea of partial order reduction is to substitute the equivalent interleavings with a single representative trace to reduce the number of states to discover. The technique builds on the explicit approach, so most of the methods used there remain applicable.

Another way of handling the state-space explosion is directed model checking. The method performs well only if we know that the sought state is reachable (this can be ensured via many ways, e.g., a symbolic checking beforehand). The algorithm exploits the fact that we only have to discover a trace to the sought state and do not have to discover the whole state-space thus shrinking memory consumption. The main idea is using a heuristic function to direct the search towards the sought state, and do not perform a traditional exhaustive search.

In this work, we present a directed model checker which uses a new heuristic to guide the state-space traversal, combined with Partial Order Reduction to boost our efficiency for cases where a sought state is not reachable. The work also includes measurement results to demonstrate and evaluate our approach.

Downloads

Please sign in to download the files of this thesis.