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

Fig. 3.1 Relationship
between constructs: Machine
and Contexts

parts of the system, while Machines is used to specify dynamic behaviour of the
system. Context can be extended by other contexts and referenced by machines.
A dynamic part of the system, machines can be refined by machines. Figure 3.1
depicts basic constructs and their relationship.

3.3.1 Contexts

Contexts express the axiomatic static properties of the models. Contexts may con-
tain carrier sets (s) , constants (c) , axioms, and theorems. The carrier sets are just
represented by their name. The different carrier sets of a context are completely in-
dependent, and that are supposed to be non-empty. The constants are defined using
a set of predicates. The predicates of a system require to satisfy properties

(s, c) .
A set of axioms can describe properties of the carrier sets and the constants. Theo-
rems are derived properties that can be proved from the axioms. Proof obligations
associated with contexts are straightforward: the stated theorems must be proved,
which follow from the predefined axioms and theorems. Additionally, a context may
be indirectly seen by machines. Namely, a context C can be seen by a machine M
indirectly if the machine M explicitly sees a context which is an extension of the
context C .

P

3.3.2 Machines

A machine is a known as a formal discrete model that expresses dynamic be-
havioural properties of a system. The machine model contains a set of state variables
(x) , invariants I(x) , theorems, events (e) , and variants. A variable x represents the
state of the machine. The variables, like constants, correspond to simple mathemat-
ical objects: sets, binary relations, functions, numbers, etc. They are constrained by
invariants I(x) . Invariants I(x) are supposed to hold whenever the value of vari-
ables changes.
A machine is organising events modifying state variables, and it uses static in-
formations defined in a context. These basic structure mechanisms are extended