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.
| 
