Event-B

Event-B is a formal method and mathematical notation for the modeling of reactive and distributed systems, developed by Jean-Raymond Abrial as a successor to the classical B method. While the original B method was designed for sequential software systems with a state-based model, Event-B uses an event-driven paradigm: systems are described as a collection of events that modify state variables, guarded by conditions that determine when they can fire. This shift makes Event-B natural for modeling concurrent, reactive, and real-time systems where behavior is driven by external stimuli rather than sequential control flow. Event-B retains the core refinement methodology of its predecessor — abstract specifications are progressively refined toward implementable designs through mathematically proven steps — but extends the proof infrastructure to handle the non-determinism and interleaving inherent in concurrent systems. The Rodin platform provides an open-source integrated development environment for Event-B, supporting proof obligation generation, automatic and interactive proof, and model animation. Event-B has been applied to the verification of railway signaling systems, avionics, and communication protocols, demonstrating that the B family's approach to refinement scales beyond sequential software to the coordination problems that define modern systems engineering.