Biomedical Engineering Reference
In-Depth Information
and difficult proofs. The re-use of developed models and the structuring mecha-
nisms available in B help in decreasing the complexity. Where B has been exercised
on known difficult problems, the result has often been a simpler proof development
than has been achieved by users of other more monolithic techniques [ 33 ].
3.1.3 Scope of the B Modelling
The scope of the B method concerns the complete process of software and system
development. Initially, the B method was mainly restricted to the development of
software systems [ 11 , 26 , 30 ] but a wider scope for the method has emerged with
the incorporation of the event based approach [ 1 , 3 , 5 , 14 , 15 ] and is related to the
systematic derivation of reactive distributed systems. Events are simply expressed in
the rich syntax of the B language. Abrial and Mussat [ 5 ] introduce elements to han-
dle liveness properties. The refinement of the event-based B method does not deal
with fairness constraints but introduces explicit counters to ensure the happening of
abstract events, while new events are introduced in a refined model. Among case
studies developed in B, we can mention the METEOR project [ 11 ] for controlling
train traffic, the PCI protocol [ 18 ], the IEEE 1394 Tree Identify Protocol [ 6 ]. Finally,
B has been combined with CSP for handling communications systems [ 13 , 14 ] and
with action systems [ 15 ]. The proposal can be compared to the action systems [ 8 ],
UNITY programs [ 19 ] and TLA +
[ 28 ] specifications but there is no notion of ab-
stract fairness like in TLA +
or in UNITY.
3.1.4 Structure of This Chapter
This chapter presents basic information about Event-B modelling language. Sec-
tion 3.2 explores the related techniques and Sect. 3.3 presents the Event-B modelling
notation. Section 3.4 gives an idea about modelling actions over states, and Sect. 3.5
represents the proof obligations. Section 3.6 gives detail about model refinement,
and finally, Sect. 3.7 discusses about the decomposition approach in modelling.
3.2 Related Techniques
The B method is a state-based method integrating set theory, predicate calculus and
generalised substitution language. We briefly compare it to related notations.
Like Z [ 25 , 37 ], B is based on the ZF set theory; both notations share the same
roots, but we can point to a number of interesting differences. Z expresses state
change by use of before and after predicates, whereas the predicate transformer se-
mantics of B allows a notation which is closer to programming. Invariants in Z are
Search WWH ::




Custom Search