Event-B.org

Home of Event-B and the Rodin Platform

ACKNOWLEDGEMENTS

ADVANCE Logo

FP7 Logo

SourceForge.net Logo

ECS

YourKit

  

Book on Event-B

Modeling in Event-B: System and Software Engineering

By Jean-Raymond Abrial

Modeling in Event-B: System and Software Engineering provides a comprehensive exposition of the Event-B approach for modeling and reasoning about systems. The mathematical language and the proof method of Event-B are introduced. Through a series of realistic case studies, the important modeling and reasoning concepts are explained. Many of these case studies are inspired from the author's industrial experience and include control systems, communications protocols, distributed algorithms and digital circuits. The book can be used for an introductory course on formal modeling and reasoning and can be used for an advanced course involving more complex data structures and automated proof. The book will serve as an excellent companion to the Rodin tool.

The book is published by Cambridge University Press (see CUP web page).

Two sample chapters are available here (Copyright Jean-Raymond Abrial):

Slides and Rodin archives associated with the book are available here.

An errata sheet for the book is available here. If you spot an error in the book that is not listed here, please report it on the rodin-b-sharp-user mailing list.

Paper on the Rodin tool: Paper on the Rodin tool: 

 
@article{AbrialBHHMV10,
  author    = {Jean-Raymond Abrial and
               Michael Butler and
               Stefan Hallerstede and
               Thai Son Hoang and
               Farhad Mehta and
               Laurent Voisin},
  title     = {Rodin: an open toolset for modelling and reasoning in {Event-B}},
  journal   = {STTT},
  volume    = {12},
  number    = {6},
  year      = {2010},
  pages     = {447-466},
  ee        = {http://dx.doi.org/10.1007/s10009-010-0145-y}
}

 

 

Event-B.org