Book contents
- Frontmatter
- Contents
- Prologue: Faultless systems – yes we can!
- Acknowledgments
- 1 Introduction
- 2 Controlling cars on a bridge
- 3 A mechanical press controller
- 4 A simple file transfer protocol
- 5 The Event-B modeling notation and proof obligation rules
- 6 Bounded re-transmission protocol
- 7 Development of a concurrent program
- 8 Development of electronic circuits
- 9 Mathematical language
- 10 Leader election on a ring-shaped network
- 11 Synchronizing a tree-shaped network
- 12 Routing algorithm for a mobile agent
- 13 Leader election on a connected graph network
- 14 Mathematical models for proof obligations
- 15 Development of sequential programs
- 16 A location access controller
- 17 Train system
- 18 Problems
- Index
5 - The Event-B modeling notation and proof obligation rules
Published online by Cambridge University Press: 05 March 2013
- Frontmatter
- Contents
- Prologue: Faultless systems – yes we can!
- Acknowledgments
- 1 Introduction
- 2 Controlling cars on a bridge
- 3 A mechanical press controller
- 4 A simple file transfer protocol
- 5 The Event-B modeling notation and proof obligation rules
- 6 Bounded re-transmission protocol
- 7 Development of a concurrent program
- 8 Development of electronic circuits
- 9 Mathematical language
- 10 Leader election on a ring-shaped network
- 11 Synchronizing a tree-shaped network
- 12 Routing algorithm for a mobile agent
- 13 Leader election on a connected graph network
- 14 Mathematical models for proof obligations
- 15 Development of sequential programs
- 16 A location access controller
- 17 Train system
- 18 Problems
- Index
Summary
In previous chapters, we used the Event-B notation and the various corresponding proof obligation rules without introducing them initially in a systematic fashion. We presented them instead in the examples when they were needed. This was sufficient for the simple examples we studied because we used part of the notation and part of the proof obligation rules only. But it might not be adequate to continue in this way when presenting more elaborate examples in subsequent chapters. The purpose of this chapter is thus to correct this. First, we present the Event-B notation as a whole, in particular the bits not used so far, and then we present all the proof obligation rules. This will be illustrated with a simple running example.
The Event-B notation
Introduction: machines and contexts
The primary concept in doing formal developments in Event-B is that of a model. A model contains the complete mathematical development of a Discrete Transition System. It is made of several components of two kinds: machines and contexts. Machines contain the dynamic parts of a model, namely variables, invariants, theorems, variants, and events, whereas contexts contain the static parts of a model, namely carrier sets, constants, axioms, and theorems. This is illustrated in Fig. 5.1. Items belonging to machines or contexts (variables, invariants, etc.) are called modeling elements.
A model can contain contexts only, or machines only, or both. In the first case, the model represents a pure mathematical structure with sets, constants, axioms, and theorems.
- Type
- Chapter
- Information
- Modeling in Event-BSystem and Software Engineering, pp. 176 - 203Publisher: Cambridge University PressPrint publication year: 2010