Skip to main content.

Contents

University Example
Milner's Scheduler Example
Short Language Reference

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.


Machine automaton.

Researcher automaton.

University automaton.

Spec automaton.
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.

Variant university model.
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.

First half university model.

Second half university model.

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).

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 (0rec[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.

Sub-specification automaton.

Node automaton.

Specification automaton.
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.

Language

To define timed I/O automata, timed game automata of TIGA with the following constraints are used:

  • Invariants may not be strict.
  • Inputs must use controllable edges.
  • Outputs must use uncontrollable edges.
  • All channels must be declared broadcast.
  • The system is implicitly input enabled due to broadcast communication but for refinement checking purposes, the relevant inputs must be explicit in the model.
  • In the case of parallel composition of several components, a given output must be exclusive to one component.
  • For implementations, outputs must be urgent.
  • For implementations, every state must have independent time progress, i.e., progress must be ensured by either an output or infinite delay.
  • Tau transitions (no output or input) are forbidden.
  • Global variables are forbidden.
The grammar for specifying property is given by:
Property := 'consistency:' System | 'refinement:' System '<=' System | 'specification:' System | 'implementation:' System
System := ID | '(' System Expr ')' | '(' Composition Expr ')' | '(' Conjunction Expr ')' | '(' Quotient Expr ')'
Composition := System '||' System | Composition '||' System
Conjunction := System '&&' System | Conjunction '&&' System
Quotient := System '\' System
Expr := /* nothing */ | ':' tctl
In particular the grammar can generate expressions of the type refinement: (A || B) <= (C : A[] not C.unsafe). As a reminder the tctl formulas supported are
  • A[ p U q ]
    For all path p must be satisfied until q with the twist (due to the game setting) that p must still hold when q holds.
  • A<> q
    Equivalent to A[ true U q ].
  • A[ p W q ]
    The weak until variant.
  • A[] p
    Equivalent to A[ p W false ].
  • A[] (p && A<> q)
    This is the Büchi objective formula with safety. for all path p must always hold and q must always be reachable from all states.
  • A[] A<> q
    Equivalent to A[] (true && A<> q).
The formulas involving a Büchi objective can be used to constrain the behaviours to be non-zeno by adding an observer automata that visits a state when time elapses.