ECDAR Case Studies and Examples

• University Example
• Milner’s Scheduler Example

University Example

The university.xml example is available in the demo directory of the distribution. In this model we check if a specification is a refinement of a another specification. The first specification is given by three components put in parallel, namely a machine, a researcher, and a university. The idea is that the university should accept grants and output patents. To do so it outputs coins to a machine that feeds coffee or tee to a researcher who is going to produce publications. When publications are generated, the university generates a patent. The second specification defines the valid sequence of grants and patents.

The ‘Inconsistent’ state for the researcher is only there for testing to make sure the pruning is working. If we check the property refinement: (University || Researcher || Machine) <= Spec the property will be satisfied, which is not very interesting. If we change the university for a variant model that allows for “free” publications, then the refinement does not hold anymore. The reason is that it’s possible to have free tea, which can give free publications, but the specification Spec forbids this behaviour.

To exercise the conjunction operator we can also specify the university as a conjunction of two automata. This allows the user to specify the constraints of outputing patents and coins separately. The resulting conjunction is a better (an more complete) specification for the university but it allows for free publications too. The property refinement: ((HalfUni1 && HalfUni2) || Researcher || Machine) <= Spec does not hold. However, it is the Spec model that is wrong, not the models of the university. Adding a self loop to Spec that outputs patents from its Start initial location corrects the problem.

Milner’s Scheduler Example

The Milner-8Nodes.xml example is available in the demo directory of the distribution. A paper describing the example is available here. In brief, this model schedules n processes P(i), 0 < i < n-1, in succession modulo n (here 8). Furthermore, a process may never be reactivated before it has terminated. Every process is associated to a node in the model. The nodes receive a request, complete some task, and send a request to the next node, before or after completion. To this purpose, a node N[i] has three ports rec[i], w[i], and rec[i+1] (modulo N).

• 1. First N[i] needs to receive the token (from N[i-1]) as an input rec[i]?
• 2. In parallel, N[i]
  • a) outputs to external environment on w[i]!
  • b) passes the token to successor node N[i+i] by output rec[i+1]!Here a) should be completed before D time units and b) completed within d and D time units.

To perform compositional model-checking, a number of subspecifications SSi are used. Here SSi is a specification for N1 || .. || Ni, noting that the relevant ports for this subsystem are rec[1]?, w[e]! with (0<e<=i) and="" <code="">rec[i+1]!. We assume that (i) more than N*d time-units elapse between two rec[1]?, and (ii) no consecutive inputs rec[1]? occur without a rec[i+1]! Furthermore, it is guaranteed that after any rec[1]?, rec[i+1]! occurs between i*d and i*D time units. The generic nodes are shown in the figure below. The first node that starts the chain is slightly different. The sub-specification automaton is shown as well. As an overall specification Spec(id=0), we have that w[0]! must occur with a time separation of at most (N+1)*D.

Checking the whole system at once with the property

refinement : ( N0 || N1 || N2 || N3 || N4 || N5 || N6 || N7 ) <= S0

is hopeless. Instead we use incremental verification and we check the following sequence of properties:

refinement : N1 <= SS1 refinement : ( SS1 || N2) <= SS2 refinement : ( SS2 || N3 ) <= SS3 refinement : ( SS3 || N4 ) <= SS4 refinement : ( SS4 || N5 ) <= SS5 refinement : ( SS5 || N6 ) <= SS6 refinement : ( SS6 || N7 ) <= SS7 And finally, using the Invariant to establish the overall property:
refinement : ( ( SS7 ) || N0) <= S0

The smaller d is, the more interleaving there will be, which can be experimented with, in particular the effect is dramatic for the first (hopeless) formula.