Event-B Language

Book: Modeling in Event-B: System and Software Engineering by Jean-Raymond Abrial

More information about the book is at Cambridge University Press website.

The Event-B introduced in Abrial's book in some ways differs from the Event-B implemented by Rodin. Some of those differences are listed here.

Sample Chapters of the Book

These are available at event-b.org.

Slides and Rodin Platform archives of the developments corresponding to chapters of the books

• Chapter 1: Introduction
• Chapter 2: Controlling Cars on a Bridge
• Chapter 3: A Mechanical Press Controller
• Chapter 4: File Transfer Protocol
• Chapter 6: The Bounded Re-transmission Protocol
• Chapter 7: Concurrent Program Development
• Chapter 8: Electronic Circuits Development
• Chapter 10: Leader Election on a Ring-shaped Network
• Chapter 11: Synchronizing Processes on a Tree Network
• Chapter 12: Routing Algorithm for Mobile Agent
• Chapter 13: The Leader Election Protocol (IEEE1394)
• Chapter 15: Sequential Program Development
• Chapter 16: Location Access Controller
• Chapter 17: Train System

Event-B Language Documentation

Event-B Modelling Language

Event-B Mathematical Language

[System Modelling & Design Using Event-B.] Draft book by Ken Robinson

Concise Summary of the Event B mathematical toolkit by Ken Robinson

Well-definedness in Event-B

Modelling Tips

Structured_Types

Proof Hints

Miscellaneous

• Jean-Raymond Abrial, "Faultless Systems: Yes We Can!," Computer, vol. 42, no. 9, pp. 30-36, Sept. 2009, doi:10.1109/MC.2009.283.