The Modelling Framework: Event-B - Using Event-B for Critical Device Software Systems - page 53

event guards/actions. The Rodin tool supports well-definedness to aid the activities
of modelling and proving [ 2 ]. The INV proof obligations are generated to guarantee
that the invariants are always preserved whenever the machine state changes. Proof
obligations ( INV 1 and INV 2 ) are produced by the Rodin tool [ 36 ] from events to
state that an invariant condition I(x) is preserved. Their general form follows imme-
diately from the definition of the before-after predicate BA(e)(x, x ) of each event
e and grd(e)(x) is safety of the guard G(t, x) of the event e :
( INV1 ) Init(x) ⇒ I(x)

BA(e)(x, x ) I(x )

( INV2 )I(x) ∧ ⇒

The generated GRD proof obligation ensures that the guard of a concrete event
is a correct refinement of the corresponding guard of the abstract event. Finally, the
generated SIM proof obligations aim to ensure that the abstract actions are refined
correctly by the action of the corresponding concrete event as specified by any glu-
ing invariants. Note that it follows from the two guarded forms of the events that
this obligation is trivially discharged when the guard of an event is false. Whenever
this is the case, the event is said to be disabled .
The proof obligation FIS expresses the feasibility of the event e with respect to
the invariant I . By proving feasibility we achieve that BA(e)(x, y) provides an after
state whenever grd(e)(x) holds. This means that the guard indeed represents the en-
abling condition of the event. The intention of specifying a guard of an event is that
the event may always occur when the guard is true. There is, however, some interac-
tion between guards and non-deterministic assignments, namely x :| BA(e)(x, x ) .
The predicate BA(e)(x, x ) of an action x

BA(e)(x, x ) is not satisfiable or the set :|

S of an action v :∈ S is empty. Both cases show violations of the event feasibility

proof obligation.

( FIS )I(x) ∧ grd(e)(x) ⇒∃ y.BA(e)(x, y)

We say that an assignment is feasible if there is an after-state satisfying the corre-
sponding before-after predicate. For each event its feasibility must be proved. Note,
that for deterministic assignments, the proof of feasibility is trivial. Furthermore,
note that feasibility of the initialisation of a machine yields the existence of an ini-
tial state of the machine. It is not necessary to require an extra initialisation.
It is sometimes useful to state that the model which has been defined is deadlock
free, that it can run for ever. This is very simply done by stating that the disjunction
of the event guards always hold under the properties of the constant and the invari-
ant. This is shown as follows, where G 1 (e)(x),..., G n (e)(x) denotes the guards of
events.

( DKLF )I(x) ⇒ G 1 (e)(x) ∨ G 2 (e)(x),..., G n (e)(x)

3.6 Model Refinement

The refinement of a formal model allows us to enrich the model via a step-by-step
approach and is the foundation of our correct-by-construction approach [ 31 ]. Re-