Modeling in Event-B: System and Software Engineering
Forthcoming book 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 will be published by Cambridge University Press in 2010 (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.
| 
