CMC Tool

Compositional Model Checking for Real-Time Systems

Compositional Model Checking

The major obstacle for the timed model-checking approach is the state explosion problem due to the parallel composition (as in the untimed case) and due to the time encoding. Several heuristics have been proposed to overcome this problem: symbolic model-checking, on-the-fly techniques, compact data-structures for time constraints. Given a network S = (A1 | ... | An) and a formula F , another possibility consists in using a compositional approach to avoid the construction of the product automaton corresponding to S = (A1 | ... | An) : the idea is to remove the component A1 from S and to encode its pertinent behavior (w.r.t. F ) into a new formula F /A1 which holds for S'=(A2 | ... | An) iff F holds for S . Now repeating this operation with other components leads to the problem of establishing that nil (a process which performs no action at all) satisfies the last formula ( F/A1.../An). The tool CMC implements this compositional model-checking. The theoretical basis of CMC can be found in the paper CMC: a tool for Compositional Model-Checking of Real-Time Systems .

Extension to Linear Hybrid Systems

An extension to linear hybrid system has been proposed in Model-checking for hybrid systems by quotienting and constraints solving . This provided: Hybrid CMC (HCMC). An implementation has been done in HCMC (Hybrid and Compositional Model Checking) for stopwatch automata. The DBM are used to overapproximate the set of configurations.

HCMC and Timed Control

In a recent paper (a research report "Modal Logics for Timed Control" is available here ), the method has been used in order to solve timed control problems. The idea is to encode the existence of timed controllers for a system as a timed modal logic formula to be checked over the system.

An example of verification with CMC

We present a classical example: the train crossing. This allows us to present the way of using CMC.
We consider a system composed by several trains , a gate and a controller. Every automaton is described as in the figure below.


In CMC, the synchronization of the automata is given explicitly in a table.
The following file contains the full description of the system: Tsystem
Verifying this system consists in deciding properties like:
These properties can easily be expressed with Lnu -- a timed modal logic -- handled by CMC. The following file contains all these properties: Tprop
Now the verification procedure can be called by typing: Verify(F1,S,T); and Verify(F1,S,T); and Verify(F1,S,T);

An example of timed control

Now the aim is: given the description of the trains and the gate, does there exist a controller (which outputs signals GoUp and GoDown ) in order to satisfy the following properties:
We look for a dense-time control: the controller can prevent time elapsing and force a controllable action to happen at any point in time. We just require that there are at least D time units between two controllable actions.
Let C be the self-loop automaton generating controllable actions s.t. at least D time units separate these actions. We can then reduce the existence of a controller to a model checking problem for (Train | Train | Gate | C ) and the following formula: Note that the modalities of Lnu are not sufficient to express dense time control, and we need to use the modality [@) (its semantics is defined in the research report mentioned above). The formula X1 defined as follows expresses the existence of a dense-time controller for the train crossing:

X1 = (*:ON => gate:CLOSE) ^ [App] X1 ^ [i] X1 ^ [Exit] (z in X2) ^ X1 [@) ( < ac > X1) ;
X2 = (gate:OPEN ^ X1) v ((*:ON => gate:CLOSE) ^ z < 50 ^ [Exit] (z in X2) ^ [i] X2 ^ [App] X1 ^ X2 [@) ( < ac > X2))

Indeed the formula holds for (Train | Train | Gate | C ) : there exists a controller for the system w.r.t. the properties P1 and P2. Note that such a controller would be more efficient than the one presented in the previous section because it opens the gate sooner after the reception of an Exit signal.
Note that this formula ensures the existence of a controller, it does not provide it (see the research report for a discussion about this point).
The file of this example is available here

Simple example

The following example allows us to illustrate the different kinds of controller we can consider.
Consider the following automaton:

The aim is to avoid the state "bad". Clearly there is a strategy for this. It is sufficient to let time elapse during T time units with 10 < T < 15 and then perform the controllable transition c.
The existence of a dense-time controller is done by using a selfloop automaton performing c actions separated by at least D t.u. And we can verify the following formula over the system:

X1 = - P:BAD ^ [a] X1 ^ X1 [@) (- P:BAD ^ [a] X1 ^ < c > X1)

This allows us to show that there exists a dense time controller for D = 8.

Sampling control

In this case we look for a discrete controller: it can only react at dates which are multiples of some fixed rate D. In this case, we can use a standard Lnu formula to state the existence of a sampling controller:

X1 = - P:BAD ^ [a] X1 ^ ([c] ff v < c > X1) ^ [@] X1

In this case the power of the controller for the time elapsing is fixed in the self-loop automaton where the controllable actions are performed exactly every D t.u. Note that we add an dummy action eps in case where no active controllable action has to be performed at time D.
For the sampling control, we can show that no controller exist for D=8, but it is possible when D=3 for example. Clearly dense-time control is more general than sampling control.

Here the files for these examples: dense time and sampling

Download

The tool HCMC is available. It is written in C++, it uses bison and flex. It works on Linux and MacOs X: HCMC tool
fl at lsv.ens-cachan.fr