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

Chapter 3
The Modelling Framework: Event-B
Abstract This chapter presents an overview of the Event-B notations that are
used to formalise the cardiac pacemaker case study. Event-B has evolved from the
Classical B for specifying and reasoning about reactive systems. Main motivation
to select Event-B is targeted at an incremental modelling style where a system is
defined abstractly, and later interesting properties are introduced in an incremental
fashion using a stepwise refinement. The use of refinement represents a system at
different levels of abstraction and the use of mathematical proof verifies consistency
between the refinement levels. Event-B is an event-based approach which is defined
in terms of a few simple concepts describing a discrete event system and proof
obligations that permit verification of properties of an event system. This chapter
explains the fundamental concepts and formal notations of Event-B modelling lan-
guage. Event-B is provided with tool support in the form of an open and extensible
Eclipse-based IDE called Rodin, which is a platform for the Event-B specification
and verification.
3.1 Introduction
3.1.1 Overview of B
Classical B is a state-based method developed by Abrial for specifying, design-
ing and coding software systems. It is based on Zermelo-Fraenkel set theory with
the axiom of choice. Sets are used for data modelling, Generalised Substitutions
are used to describe state modifications, the refinement calculus is used to relate
models at varying levels of abstraction, and there are a number of structuring mech-
anisms (machine, refinement, implementation), which are used in the organisation
of a development. The first version of the B method is extensively described in The
B-book [ 2 ]. It is supported by the Atelier B tool [ 21 ] and by the B Toolkit [ 10 ].
Central to the classical B approach is the idea of a software operation which will
perform according to a given specification if called within a given pre-condition.
Subsequent to the formulation of the classical approach, Abrial and others have
developed a more general approach in which the notion of event is fundamental. An