Antti's State Space Exploration Tool (ASSET)

2017-08-30 (under construction)

What is it?How to get and run itOn modellingGetting familiar by developing the alternating bit protocolOther helpful models

What is it?

ASSET is a tool for model checking (a.k.a. automatically verifying) models of concurrent systems, such as telecommunication protocols and embedded systems. ASSET is based on constructing and analysing the set of states that the model can reach. Models are expressed as C++ code that obeys certain conventions. A model is checked by copying it to the file asset.model and then compiling and executing the file

This approach facilitates very fast construction of the reachable states. It also makes the modelling very flexible, because most features of C++ are available. On the other hand, this way of expressing models does not always support intuition well. However, ASSET can be applied to other modelling languages by implementing a preprocessor tool that inputs the other language and produces a file that is suitable for ASSET.

ASSET can check so-called safety, deadlock, and two kinds of progress properties, called here may progress and must progress. To check safety, the user must define a function that tells whether the current state is good or bad. To check deadlocks, the user must define a function that tells whether termination is allowed in the current state.

To check may progress, the user must define a function that tells whether the current state is a may progress state. By default, ASSET treats also all terminal states as may progress states, but this can be switched off. (The idea behind the default is that the terminal states may be checked via the deadlock checking feature, and it finds the errors faster.) ASSET checks that from every reachable state, a may progress state is reachable. Experts in model checking know this as verifying AG EF progress.

May progress has the advantage that it can be meaningfully used without the need to make (and thus understand) so-called fairness assumptions. It corresponds to the global fairness assumption that if a choice situation repeats infinitely often, then each alternative is chosen infinitely often. Even when one wants to use another progress concept, may progress can be used as an approximation that never yields false alarms but may miss true alarms.

Checking of must progress is otherwise similar, but ASSET checks that every cycle of reachable states contains at least one must progress state, and that every reachable terminal state is a must progress state. Experts in model checking know this as catching non-progress cycles, which are a special case of linear-time liveness errors. Often checking must progress requires fairness assumptions to avoid false alarms, but, unfortunately, ASSET does not support them. By default, ASSET treats also all terminal states as must progress states, but this can be switched off.

When ASSET finds an error, it prints a counterexample. For safety errors and illegal deadlocks, it is a sequence of states that arises from an execution of the model that starts at the initial state and leads to the error state. In the case of may or must progress, it is a sequence of states to a state that violates the progress property, followed by a sequence of states to a cycle of states or a terminal state, followed by the cycle or terminal state. In all cases, the sequence from the initial state to the error state is as short as possible. In the case of may and must progress, the rest of the counterexample has not been minimized.

With may progress, the last parts of the counterexample may seem somewhat artificial. The idea is that by analysing them, the user finds a point where the model cannot do what the user expects it to do.

ASSET can use the well-known symmetry method and/or the (strong) basic stubborn set method to reduce the number of states that are constructed. However, their use requires that the user or the preprocessor tool analyses the model and gives the necessary symmetry representative function and/or stubborn set obligation function. For the symmetry method to work correctly, the checking and progress state functions must yield the same reply on symmetric states. Furthermore, the stubborn set method is not guaranteed to find must progress errors, and the finding of safety and may progress errors is only guaranteed for may-terminating models, that is, models that cannot reach a state from which no terminal state is reachable. If the stubborn set method fails to find errors but the result cannot be trusted for the above reasons, then ASSET gives a warning.

ASSET constructs the reachable states in breadth-first order, to minimize the length of counterexamples. If a safety or deadlock error is encountered during the construction of states, ASSET reports the error and terminates. That is, ASSET may terminate before having constructed all reachable states. If no safety and deadlock errors are found and ASSET has further checks to do, it runs a backward transition construction phase that generates information needed later. Then, if the user has defined a may progress function, ASSET continues by checking may progress. If that check fails, ASSET reports the error and terminates. Otherwise, if the user has defined a must progress function, ASSET does the corresponding check. Finally, if the stubborn set method is used for detecting other than deadlock errors, ASSET checks whether the model is may-terminating.

How to get and run it

ASSET is a C++ file that #includes the model as another C++ file named asset.model. Model checking takes place by compiling and executing

You can download ASSET from here. You can freely use it for educational and research purposes, and for fun. Instead of delivering it to others, please ask them to download it from this web page, to be sure to get the most recent version. If you use it when writing scientific papers, please cite this publication: (no publication exists at the time of writing, so please cite this web page.)

It is a good idea to write a small script that copies the model to asset.model, runs the C++ compiler, and runs ASSET. This is one of the scripts that I use:

cp $1 asset.model
g++ -ansi -W -Wall -pedantic -O2 $2 -o asset.out

The first command line parameter is the name of the file that contains the model. The second parameter is optional. For instance, it can be -Donly_typical, switching the model checking off and instead printing a typical execution sequence of the model. This is very useful in early stages of writing the model, until it gets to the point where it does something reasonable.

On modelling

At the idea level, a model consists of a state and transitions.

The state consists of zero or more variables of the type state_var. When declaring a state variable, the modeller may tell how many bits it has. The default is eight bits. The value of a state variable of b bits is an unsigned integer less than 2b.

Here is an example that makes x have two bits, y have eight bits, z have one bit, and A be an array of four state variables of three bits each:

state_var x(2), y, z = 1, A[4] = 3;

In heavy model checking tasks, it is often advantageous to not use more bits than necessary for each state variable. ASSET packs the next state variable into the same machine word with the previous ones, if many enough bits are still available in the word. The user may improve this optimization by declaring the state variables in a suitable order. In a 32-bit machine,

state_var x(1), y[16] = 2, z(1);

consumes three machine words, but

state_var y[16] = 2, x(1), z(1);

consumes only two.

Also ordinary C++ variables can be declared, but they will not be part of the state.

The model must contain a print_state function that prints the state in a human-readable form. ASSET calls it when printing counterexamples.

The model starts at the initial state and makes progress by executing transitions. Unless the modeller specifies otherwise, the initial state is the one where the value of each state variable is 0. The execution of a transition typically changes the state of the model. It corresponds to an atomic action of the model. A transition may also be disabled, that is, not executable in the current state. The opposite of “disabled” is enabled.

Each transition has a number. The details of the numbering are largely unimportant. Even if two things seem logically as two different transitions, it is okay to give them the same number, if they cannot be enabled simultaneously.

The model must contain a nr_transitions function that returns the total number of transitions as an unsigned integer. If some state variables must have non-zero initial values, the desired values may be assigned in nr_transitions.

Transitions are expressed as the function fire_transition that inputs the number of a transition as an unsigned integer and returns a Boolean value. If the transition is enabled, fire_transition changes the state according to the execution of the transition and returns true. Otherwise, fire_transition returns false. In the latter case, it must not change the state. Often, but not always, fire_transition contains one or more switch statements that direct the execution to the right place in program code, given the number of the transition.

ASSET uses some heuristics that assume that the transitions have been numbered in a suitable order. Transitions that represent “successful” events, such as the reception of a message, should be given smaller numbers than transitions that represent “unsuccessful” events, such as the loss of a message. This is only a recommendation. Violating it may reduce the readability of the model checking results and increase (or decrease!) the time that it takes before the model checker finds an error, but this is usually not important.

To catch safety errors, the model must contain the function check_state. It the state is bad, the function returns a character string that tells what is wrong with the state. The character string could be "Received wrong message", for instance. ASSET prints the character string as a part of the error message. If the state is good, check_state returns the null pointer. To switch the checking of safety errors on, the model must contain #define chk_state or the same effect must be obtained via a compiler option. With the Gnu C++ compiler, the option is -Dchk_state.

If the checking of deadlocks has been switched on, ASSET calls check_deadlock on each state that it has found and that has no enabled transitions. The checking is switched on via #define chk_deadlock or a compiler option. The function returns either a character string that describes the error, or the null pointer to indicate that it is okay for the model to terminate in the state.

Checking may progress is switched on by #define chk_may_progress or with a compiler option. The modeller must have provided the function is_may_progress that returns a Boolean value. Must progress works similarly.

For more information on how to write models, please see the example models and the long initial comment in Links to the example models are further down this web page.

Other helpful models

Antti Valmari