Description

Model checking [2] is a fully automatic technique that allows to check if a given concurrent system satisfies a property like, for example, the absence of deadlocks, the absence of starvation, the fulfilment of an invariant, etc. The use of this technique is a must when developing software that controls critical systems, such as an airplane or a spacecraft. However, the memory required for the verification usually grows in an exponential way with the size of the system to verify (state explosion problem).

When the search for errors with a low amount of computational resources (memory and time) is a priority (e.g., in the first stages of the development), non-exhaustive algorithms using heuristic information can be used. In this case metaheuristic algorithms can be applied to find short error trails of software models.

The problem of finding errors in software models can be translated into the search of a path in a graph (the Büchi automaton) starting in the initial state and ending in an objective node (accepting state) and an additional cycle involving the objective node. We can formalize the problem as follows.

Let G=(S,T) be a directed graph where S is the set of nodes and T is the set of arcs. Let q be the initial node of the graph and F a set of distinguished nodes that we call final nodes. We denote with T(s) the successors of node s. A finite path over the graph is a sequence of nodes π = s₁ s₂ ... s_nwhere s_i are states and s_i belongs to T(s_i-1) for i=2,...,n. We denote with π_i the i-th node of the sequence and we use |π| to refer to the length of the path, that is, the number of nodes of π. We say that a path π is a starting path if the first node of the path is the initial node of the graph, that is, π₁=q. We will use π* to refer to the last node of the sequence π, that is, π* = π_|π|. We say that a path π is a cycle if the first and the last nodes of the path are the same, that is, π₁=π*.

Given a directed graph G, the problem at hand consists in finding a starting path π ending in an final node plus a cycle ν containing the final node. That is, find π and ν subject to π₁ = q, π* belongs to F and π*=ν₁=ν*.

The graph G used in the problem is derived from the Büchi automaton B (synchronous product of the concurrent system and the never claim in Spin). The set of nodes S in G is the set of states in B, the set of arcs T in G is the set of transitions in B, the initial node q in G is the initial state in B, and the set of final nodes F in G is the set of accepting states in B. For more details see [1,3].

Promela models

With the Spin and HSF-Spin source code a lot of Promela models can be found. In addition, there exists a benchamark with more than 300 software models (BEEM). The Spin source code can be downloaded from here and the HSF-Spin source code from here. The BEEM benchmark can be found here.

Related Bibliography and Papers