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

incorporated into operation descriptions and alter their meaning, whereas the invari-
ant in B is checked against the state changes described by operations and events
to ensure consistency. Finally, B makes a careful distinction between the logical
properties of pre-conditions and guards, which are not clearly distinguished in Z.
The refinement calculus used in B for defining the refinement between models in
the event-based B approach is very close to Back's action systems, but tool support
for action systems appears to be less mechanised than B.
TLA + [ 29 , 32 ] can be compared to B, since it includes set theory with the
operator of Hilbert. The semantics of TLA + temporal operator is expressed over
traces of states whereas the semantics of B actions is expressed in the weakest pre-
condition calculus. Both semantics are equivalent with respect to safety properties,
but the trace semantics of TLA + allows an expression of fairness and eventuality
properties that is not directly available in B.
VDM [ 23 , 27 ] is a method with similar objectives to classical B. Like B it uses
partial functions to model data, which can lead to meaningless terms and predicates,
e.g. when a function is an applied outside its domain. VDM uses a special three val-
ued logic to deal with indefiniteness. B retains classical two valued logic, which
simplifies proof at the expense of requiring more care with indefiniteness. Recent
approaches to this problem will be mentioned later. ASM [ 12 , 24 , 35 ] and B share
common objectives related to the design and the analysis of (software/hardware)
systems. Both methods bridge the gap between human understanding and formula-
tion of real-world problems and the deployment of their computer-based solutions.
Each has a simple scientific foundation: B is based on set theory, and ASM is based
on the algebraic framework with an abstract state change mechanism. An Abstract
State Machine is defined by a signature, an abstract state, a finite collection of rules
and a specific rule; rules provide an operational style very useful for modelling spec-
ification and programming mechanisms. Like B, ASM includes a refinement relation
for the incremental design of systems; the tool support of ASM is under develop-
ment, but it allows one to verify and to analyse ASMs. In applications, B seems to
be more mature than ASM, even if ASM has several real successes like the valida-
tion [ 38 ] of Java and the Java Virtual Machine.
3.3 The Event-B Modelling Notation
Event-B [ 4 ], unlike Classical B [ 2 ], does not have a fixed syntax. We summarise
the concepts of the Event-B modelling language [ 4 , 17 ] developed by Abrial and
indicate the links with the tool called Rodin [ 36 ]. Here, we present the basic notation
for Event-B using some syntax. We proceed like this to improve legibility and help
the reader remembering the different constructs of Event-B. The syntax should be
understood as a convention for presenting Event-B models in a textual form rather
than defining a language.
Event-B [ 4 ] modelling language has mainly two main constructs contexts and
machines , which are used to model a system. Contexts is used to formalise the static