You are previewing Modeling in Event-B.
O'Reilly logo
Modeling in Event-B

Book Description

A practical text suitable for an introductory or advanced course in formal methods, this book presents a mathematical approach to modelling and designing systems using an extension of the B formal method: Event-B. Based on the idea of refinement, the author's systematic approach allows the user to construct models gradually and to facilitate a systematic reasoning method by means of proofs. Readers will learn how to build models of programs and, more generally, discrete systems, but this is all done with practice in mind. The numerous examples provided arise from various sources of computer system developments, including sequential programs, concurrent programs and electronic circuits. The book also contains a large number of exercises and projects ranging in difficulty. Each of the examples included in the book has been proved using the Rodin Platform tool set, which is available free for download at www.event-b.org.

Table of Contents

  1. Cover
  2. Title Page
  3. Copyright
  4. Contents
  5. Prologue: Faultless systems – yes we can!
  6. Acknowledgments
  7. 1. Introduction
    1. 1.1 Motivation
    2. 1.2 Overview of the chapters
    3. 1.3 How to use this book
    4. 1.4 Formal methods
    5. 1.5 A little detour: blueprints
    6. 1.6 The requirements document
    7. 1.7 Definition of the term “formal method” as used in this book
    8. 1.8 Informal overview of discrete models
    9. 1.9 References
  8. 2. Controlling cars on a bridge
    1. 2.1 Introduction
    2. 2.2 Requirements document
    3. 2.3 Refinement strategy
    4. 2.4 Initial model: limiting the number of cars
    5. 2.5 First refinement: introducing the one-way bridge
    6. 2.6 Second refinement: introducing the traffic lights
    7. 2.7 Third refinement: introducing car sensors
  9. 3. A mechanical press controller
    1. 3.1 Informal description
    2. 3.2 Design patterns
    3. 3.3 Requirements of the mechanical press
    4. 3.4 Refinement strategy
    5. 3.5 Initial model: connecting the controller to the motor
    6. 3.6 First refinement: connecting the motor buttons to the controller
    7. 3.7 Second refinement: connecting the controller to the clutch
    8. 3.8 Another design pattern: weak synchronization of two strong reactions
    9. 3.9 Third refinement: constraining the clutch and the motor
    10. 3.10 Fourth refinement: connecting the controller to the door
    11. 3.11 Fifth refinement: constraining the clutch and the door
    12. 3.12 Another design pattern: strong synchronization of two strong reactions
    13. 3.13 Sixth refinement: more constraints between clutch and door
    14. 3.14 Seventh refinement: connecting the controller to the clutch buttons
  10. 4. A simple file transfer protocol
    1. 4.1 Requirements
    2. 4.2 Refinement strategy
    3. 4.3 Protocol initial model
    4. 4.4 Protocol first refinement
    5. 4.5 Protocol second refinement
    6. 4.6 Protocol third refinement
    7. 4.7 Development revisited
    8. 4.8 Reference
  11. 5. The Event-B modeling notation and proof obligation rules
    1. 5.1 The Event-B notation
    2. 5.2 Proof obligation rules
  12. 6. Bounded re-transmission protocol
    1. 6.1 Informal presentation of the bounded re-transmission protocol
    2. 6.2 Requirements document
    3. 6.3 Refinement strategy
    4. 6.4 Initial model
    5. 6.5 First and second refinements
    6. 6.6 Third refinement
    7. 6.7 Fourth refinement
    8. 6.8 Fifth refinement
    9. 6.9 Sixth refinement
    10. 6.10 Reference
  13. 7. Development of a concurrent program
    1. 7.1 Comparing distributed and concurrent programs
    2. 7.2 The proposed example
    3. 7.3 Interleaving
    4. 7.4 Specifying the concurrent program
    5. 7.5 Refinement strategy
    6. 7.6 First refinement
    7. 7.7 Second refinement
    8. 7.8 Third refinement
    9. 7.9 Fourth refinement
    10. 7.10 Reference
  14. 8. Development of electronic circuits
    1. 8.1 Introduction
    2. 8.2 A first example
    3. 8.3 Second example: the arbiter
    4. 8.4 Third example: a special road traffic light
    5. 8.5 The Light circuit
    6. 8.6 Reference
  15. 9. Mathematical language
    1. 9.1 Sequent calculus
    2. 9.2 The propositional language
    3. 9.3 The predicate language
    4. 9.4 Introducing equality
    5. 9.5 The set-theoretic language
    6. 9.6 Boolean and arithmetic language
    7. 9.7 Advanced data structures
  16. 10. Leader election on a ring-shaped network
    1. 10.1 Requirement document
    2. 10.2 Initial model
    3. 10.3 Discussion
    4. 10.4 First refinement
    5. 10.5 Proofs
    6. 10.6 Reference
  17. 11. Synchronizing a tree-shaped network
    1. 11.1 Introduction
    2. 11.2 Initial model
    3. 11.3 First refinement
    4. 11.4 Second refinement
    5. 11.5 Third refinement
    6. 11.6 Fourth refinements
    7. 11.7 References
  18. 12. Routing algorithm for a mobile agent
    1. 12.1 Informal description of the problem
    2. 12.2 Initial model
    3. 12.3 First refinement
    4. 12.4 Second refinement
    5. 12.5 Third refinement: data refinement
    6. 12.6 Fourth refinement
    7. 12.7 References
  19. 13. Leader election on a connected graph network
    1. 13.1 Initial model
    2. 13.2 First refinement
    3. 13.3 Second refinement
    4. 13.4 Third refinement: the problem of contention
    5. 13.5 Fourth refinement: simplification
    6. 13.6 Fifth refinement: introducing cardinality
  20. 14. Mathematical models for proof obligations
    1. 14.1 Introduction
    2. 14.2 Proof obligation rules for invariant preservation
    3. 14.3 Observing the evolution of discrete transition systems: traces
    4. 14.4 Presentation of simple refinement by means of traces
    5. 14.5 General refinement set-theoretic representation
    6. 14.6 Breaking the one-to-one relationship between abstract and concrete events
  21. 15. Development of sequential programs
    1. 15.1 A systematic approach to sequential program development
    2. 15.2 A very simple example
    3. 15.3 Merging rules
    4. 15.4 Example: binary search in a sorted array
    5. 15.5 Example: minimum of an array of natural numbers
    6. 15.6 Example: array partitioning
    7. 15.7 Example: simple sorting
    8. 15.8 Example: array reversing
    9. 15.9 Example: reversing a linked list
    10. 15.10 Example: simple numerical program computing the square root
    11. 15.11 Example: the inverse of an injective numerical function
  22. 16. A location access controller
    1. 16.1 Requirement document
    2. 16.2 Discussion
    3. 16.3 Initial model of the system
    4. 16.4 First refinement
    5. 16.5 Second refinement
    6. 16.6 Third refinement
    7. 16.7 Fourth refinement
  23. 17. Train system
    1. 17.1 Informal introduction
    2. 17.2 Refinement strategy
    3. 17.3 Initial model
    4. 17.4 First refinement
    5. 17.5 Second refinement
    6. 17.6 Third refinement
    7. 17.7 Fourth refinement
    8. 17.8 Conclusion
    9. 17.9 References
  24. 18. Problems
    1. 18.1 Exercises
    2. 18.2 Projects
    3. 18.3 Mathematical developments
    4. 18.4 References
  25. Index