Awesome Event-B

A curated list of resources for the Event-B formal method and the Rodin platform.

Event-B is a formal method for system-level modelling and analysis. It uses set theory as a notation, refinement to relate models at different levels of abstraction, and mathematical proof to verify their consistency. Models are built and proofs discharged in the open, Eclipse-based Rodin platform. The method was created by Jean-Raymond Abrial and is widely applied to safety-critical systems such as railway signalling.

Contents

• Official Resources
• Tools
  • Platform
  • Command-Line and Tooling
  • Editors
  • Provers and Verification
  • Animation and Visualization
  • Modelling Extensions
  • Code Generation
  • Requirements and Documentation
• Books
• Cheat Sheets and Reference
• Tutorials
• Models and Examples
• Papers
  • Foundations and Methodology
  • Tools and Verification
  • Applications and Case Studies
• Standards
• Conferences
• Community
• Industrial Use
• Related

Official Resources

• Event-B and Rodin Wiki - Community-maintained hub for the language, platform, tutorials, and plugins.
• Event-B Language - Reference for the Event-B mathematical notation and model structure.
• Rodin Platform Welcome Page - Starting point with downloads and getting-started material.
• Rodin Platform Releases - Version history and release notes for the Rodin toolset.
• Event-B on Wikipedia - Concise encyclopedic introduction to the method and its background.

Tools

Platform

• Rodin - Eclipse-based IDE for modelling, refinement, and proof in Event-B.
• RodinCore - Source repository for the Rodin platform core.
• Rodin Plug-ins - Index of available plugins with descriptions and install sites.

Command-Line and Tooling

• Rossi - Rust toolchain for Event-B with a parser, type checker, CLI, and language server that round-trips with Rodin.
• rodin-headless - Headless toolchain to build, model-check, and prove Rodin Event-B models from the command line or Docker.
• eventb-animate - Command-line tool to animate Event-B models with ProB without Rodin.
• eventb-checker - Command-line validator for Event-B models, also available as a GitHub Action.
• eventb-to-txt - Converts Event-B machines and contexts to CamilleX plain-text models.
• tree-sitter-eventb - Tree-sitter grammar for the Event-B textual syntax, generated from Rossi.

Editors

• Event-B for VS Code - VS Code extension for Event-B with syntax highlighting and the Rossi language server, also on Open VSX.

Provers and Verification

• SMT Solvers Plug-in - Discharges proof obligations using external SMT solvers.
• Isabelle for Rodin - Integrates the Isabelle/HOL prover with Event-B proofs.

Animation and Visualization

• ProB - Animator and model checker for Event-B, B, Z, TLA+, and CSP.
• ProB2-UI - Modern JavaFX interface for the ProB animator and model checker.
• VisB - Adds lightweight SVG-based visualizations to formal models.
• SimB - Timed, probabilistic simulation of Event-B models.
• AnimB - Animator for stepping through Event-B models inside Rodin.
• BMotionWeb - Builds domain-specific, web-based visualizations of formal models.

Modelling Extensions

• Theory Plug-in - Extends the mathematical language with operators, datatypes, and rewrite rules.
• UML-B - Diagrammatic class- and state-machine front end for Event-B.
• CamilleX - Text-based editor and syntax extensions for Event-B.
• Records Extension - Adds structured record types to the Event-B language.
• Decomposition Plug-in - Splits a model into sub-models via shared variables or events.
• Atomicity Decomposition Plug-in - Structures the refinement of event atomicity.
• Modularisation Plug-in - Builds and proves modular Event-B developments.
• Flows Plug-in - Adds explicit control flow between events.

Code Generation

• Code Generation Activity - Overview of code generation approaches and tools for Event-B.
• Tasking Event-B - Generates multi-tasking code in Ada, Java, and C from Event-B.

Requirements and Documentation

• ProR - Links natural-language requirements to Event-B models.
• B2Latex - Typesets Event-B models as LaTeX for documents.

Books

• Modeling in Event-B: System and Software Engineering - Jean-Raymond Abrial's definitive textbook on the method.
• System Modelling and Design Using Event-B - Ken Robinson's free, book-length introductory notes on modelling with Event-B (PDF, archived).
• Rodin Handbook - Comprehensive guide to installing and using Rodin and Event-B.
• A Tool's Security Model: Formally Describing Software Subsystems - Begaev and colleagues' Russian-language ITMO University study guide on building a software security model in Event-B with iUML-B and Rodin for FSTEC certification (PDF, archived).

Cheat Sheets and Reference

• The Event-B Mathematical Language - Metayer and Voisin's formal definition of the Event-B kernel language (PDF, archived).
• Event-B Mathematical Toolkit Summary - Concise summary of the toolkit with both Rodin and ASCII notation (PDF, archived).
• Event-B Reference Card - Quick-reference card for Event-B notation and machine structure (PDF, archived).

Tutorials

• Rodin Tutorials - Index of official tutorials for Rodin and its plugins.
• ProB First Steps - Hands-on introduction to animating Event-B with ProB.
• UML-B Tutorial - Step-by-step guide to diagrammatic modelling with UML-B.

Models and Examples

• Event-B Examples - Community index of downloadable Event-B developments, from teaching to industrial.
• Industrial Projects - Wiki overview of industrial projects and companies that have applied Event-B.
• DEPLOY Examples Archive - Archived repository of 60+ Event-B case studies from the EU DEPLOY project.
• ARINC 653 - Event-B formalization of the ARINC 653 avionics OS standard that uncovered six specification issues (ISSRE 2015).
• Landing Gear System - Aircraft landing gear, the benchmark case study of ABZ 2014, with several Event-B solutions.
• Hybrid ERTMS/ETCS Level 3 - European railway moving-block signalling, the benchmark case study of ABZ 2018.
• Adaptive Exterior Light and Speed Control - Automotive light and speed controller with a pitman-arm lever, the ABZ 2020 case study with Rodin models.
• HIMACF Access Control Model - Event-B specification of the role-based access control and information-flow model (formerly MROSL DP-model) used in Astra Linux.
• Mondex Electronic Purse - Incremental Event-B refinement of the Mondex smartcard electronic purse, a classic verification benchmark.
• CDIS Air-Traffic Information System - Event-B redevelopment of a commercial air-traffic control information system first specified in VDM.
• Reconfigurable On-Board Satellite System - Formal development and dependability assessment of a reconfigurable satellite system from the DEPLOY space pilot.
• Cruise Control System - Event-B modelling of an automotive cruise-control system used to evaluate a modelling guideline.
• Mechanical Press Controller - Refinement-based Event-B development of an industrial mechanical-press controller.

Papers

Foundations and Methodology

• Refinement, Decomposition, and Instantiation of Discrete Models - Abrial and Hallerstede's foundational account of refinement, decomposition, and generic instantiation in Event-B.
• An Open Extensible Tool Environment for Event-B - Early paper introducing the extensible Event-B tool environment that grew into the Rodin platform.
• On the Purpose of Event-B Proof Obligations - Hallerstede's explanation of how Event-B's proof obligations encode the method's semantics.
• The Logic of Event-B - Schmalz's specification of Event-B's abstract syntax, three-valued semantics, and proof calculus (ETH Technical Report 698).
• Term Rewriting in Logics of Partial Functions - Schmalz's report on rewriting and well-definedness in the partial-function logic underlying Event-B proofs.
• Reasoning about Liveness Properties in Event-B - Hoang and Abrial's proof rules for liveness properties under Event-B refinement.
• Decomposition Structures for Event-B - Butler's atomicity decomposition and event-refinement diagrams for structuring large refinements.
• Practical Theory Extension in Event-B - Butler and Maamria on the Theory plug-in for extending Event-B's mathematical language.
• Faultless Systems: Yes We Can! - Abrial's manifesto arguing that proof-based development can deliver fault-free systems.
• Jean-Raymond Abrial: A Scientific Biography of a Formal Methods Pioneer - Biography of the creator of Z, B, and Event-B.

Tools and Verification

• Rodin: an open toolset for modelling and reasoning in Event-B - Seminal paper describing the Rodin platform.
• ProB: A Model Checker for B - Leuschel and Butler's widely cited model checker and animator for B and Event-B.
• ProB: An Automated Analysis Toolset for the B Method - Journal account of the ProB toolset for animation, model checking, and refinement checking.
• Integrating SMT Solvers in Rodin - Deharbe and colleagues on discharging Event-B proof obligations with SMT solvers.
• Automatic Code Generation from Event-B Models - Mery and Singh's EB2ALL approach to generating C, C++, Java, and C# from Event-B models.

Applications and Case Studies

• Applying a Formal Method in Industry: a 25-Year Trajectory - Experience report on B and Event-B in industrial projects.
• Dependability-Explicit Engineering with Event-B - Overview of achievements from the EU DEPLOY project.
• An Incremental Development of the Mondex System in Event-B - Butler and Yadav's refinement-based development of the Mondex electronic purse, a verification benchmark.
• A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol - Abrial, Cansell, and Mery's proved development of the FireWire tree-identify protocol.
• Pacemaker's Functional Behaviors in Event-B - Mery and Singh's incremental Event-B model of a cardiac pacemaker's functional behaviour.
• Event-Based Formalization of ARINC 653 using Event-B - Zhao and colleagues' formalisation of the ARINC 653 avionics OS standard (ISSRE 2015).
• Security Policy Modeling and Verification - ISP RAS work on Event-B modelling of operating-system access-control policies.

Standards

• CENELEC EN 50128:2011+A2:2020 - European railway-software standard whose informative Annex D.28.9 describes Event B as the system-modelling branch of the B method. The current successor, EN 50716:2023, retains the B method.
• IEC 62279:2015 - International counterpart to EN 50128; informative Annex D.28.9 contains the same explicit description of Event B.
• GOST R IEC 62279-2016 - Active, identical Russian adoption of IEC 62279:2015 for railway software. Its Annex D.28.10 explicitly describes Event-B as “Событие B”.
• GB/T 28808-2021 - Current Chinese railway-software standard and modified adoption of IEC 62279:2015. Its informative Annex B corresponds to IEC Annex D, including the Event B description.
• NITE Railway Accreditation Scope - Japanese accreditation scope that includes IEC 62279:2015; an IPA case-study report separately documents Event-B and Rodin use in Japan.
• GOST R 59453.1-2021 - Russian national standard on the formal access-control model, general provisions.
• GOST R 59453.2-2021 - Companion standard that recommends Event-B among formalization methods and Rodin as an example tool, with worked Event-B verification examples.

Conferences

• ABZ - Conference for state-based methods including ASM, Alloy, B, TLA, VDM, Z, and Event-B.
• Formal Methods Europe - Organisation behind the FM and integrated formal-methods conferences.

Community

• Mailing Lists - Announce, user, and developer lists for Rodin and Event-B.
• Rodin User List Archive - Searchable archive of the Rodin user mailing list.
• HHU STUPS - Research group developing ProB and related Event-B tooling.

Industrial Use

• Systerel - Company leading Rodin platform development and formal verification services.
• ClearSy - Engineering firm applying B and Event-B to railway safety systems.
• openETCS Model Evaluation - Event-B models from the openETCS railway standardisation initiative.
• AstraVer Toolset - ISP RAS toolset that verifies Astra Linux security modules, pairing C deductive verification with Event-B security-policy models in Rodin.

Related

• Awesome TLA+ - Curated list for the TLA+ formal specification language.
• Atelier B - Industrial toolset for the classical B method, Event-B's predecessor.
• TLA+ - Leslie Lamport's language for specifying concurrent and distributed systems.
• Alloy - Lightweight relational modelling language and analyzer.
• Overture (VDM) - Tool support for the Vienna Development Method.
• Z notation - Specification language based on set theory and predicate logic.

Contributing

Contributions are welcome. Please read the contribution guidelines first.