Event-B

Origin. Jean-Raymond Abrial, developed through the EU RODIN (2004–2007) and DEPLOY (2008–2012) projects and set out in Modeling in Event-B: System and Software Engineering (Cambridge, 2010). Retains the B Method's typed set theory and drops its Generalised Substitution Language along with the operation-call model. Foundation of the Rodin platform.

Models. A machine is a labelled transition system presented syntactically. State is a set of variables constrained by an invariant; behaviour is a set of events, each a guarded nondeterministic assignment. The change from B is that an event is not called: when its guard is false it simply does not occur, so nothing ever executes outside its domain and B's abort semantics disappears. The static part — carrier sets, constants, axioms — is separated into contexts, which machines see. Development proceeds by refinement chains starting from a model small enough to state the requirement in a line, each layer introducing detail and its own small obligations.

Formalism.

Machine structure: MACHINE M SEES Context VARIABLES v INVARIANTS I EVENTS e = ... END

Context: CONTEXT C SETS S CONSTANTS c AXIOMS A END

Event structure: EVENT e ANY x WHERE G(x, v) THEN v := E(x, v) END

Components: WHERE: guard — a false guard blocks the event, it does not abort. THEN: action, deterministic (v := E) or nondeterministic (v :∈ S, v :| BA(v, v')). ANY: local parameters, existentially quantified over the guard and action. WITNESS: supplies the abstract parameter a refinement has dropped.

Proof obligations: INV: A ∧ I ∧ G ∧ BA ⇒ I(v') — each event preserves the invariant. FIS: A ∧ I ∧ G ⇒ ∃v'· BA(v, v') — the action is feasible where the guard holds. GRD: concrete guard ⇒ abstract guard — refinement may only block more. SIM: the concrete action simulates the abstract one across the gluing invariant. WD: well-definedness — a partial function is applied only inside its domain. VAR / NAT: the variant is a natural number and strictly decreases. THM: stated theorems follow from the axioms and invariants.

Refinement patterns: Superposition: add variables, keep the abstract ones. Data refinement: replace abstract variables, relate by a gluing invariant. Event splitting and merging. New events, which refine skip and must not take over forever.

Convergence: VARIANT V — a natural number expression or a finite set. Convergent new events must strictly decrease V. Anticipated events must not increase it, deferring the obligation to a later refinement. No infinite sequence of new events; the abstract machine keeps making progress.

Deadlock freedom (optional, stated not implied): I ⇒ (G₁ ∨ … ∨ Gₙ) — some event is always enabled.

Rodin platform: Eclipse-based; generates the obligations above and discharges them by automatic and interactive provers. ProB plugin for animation and model checking.

Symbols.

Symbol	Unicode	Name	Meaning
:=	—	Becomes equal to	Deterministic assignment in an action
:∈	—	Becomes an element of	Nondeterministic choice from a set
:\|	—	Becomes such that	Action given by a before-after predicate
∈	U+2208	Element of	Set membership, primitive of the data language
v'	—	Primed variable	Value of v after the event (apostrophe U+0027)
⇒	U+21D2	Rightwards double arrow / Implication	Shape of every proof obligation
∧	U+2227	Logical and	Conjoins axioms, invariant, and guard
∨	U+2228	Logical or	Disjunction of guards in deadlock freedom
∃	U+2203	There exists	Feasibility: some after-state exists
∀	U+2200	For all	Quantifier in invariants and axioms
ℕ	U+2115	Natural numbers	Codomain of the convergence variant
A	—	Axioms	Static properties, declared in a context
I	—	Invariant	State predicate every event must preserve
G	—	Guard	Enabling condition of an event
BA	—	Before-after predicate	Relation between v and v' effected by the action
V	—	Variant	Convergence measure for new events
INV, FIS, GRD, SIM, WD	—	Obligation names	The generated proof obligations

Metatheory. The semantics is a labelled transition system, and refinement is proved by forward simulation against a gluing invariant: the GRD obligation forces the concrete guard to imply the abstract one and SIM forces the concrete action to be matched by an abstract step, so every concrete behaviour projects to an abstract behaviour and safety properties transfer downward through the chain. Refinement is transitive, which is what licenses developing a system in many small layers instead of one large step. The obligations are generated syntactically and are individually first-order, which is why Rodin can discharge most of them automatically despite the underlying logic being undecidable. Two features distinguish the system from B. Guards replace preconditions, so an event is never taken outside its domain and the abort case never arises. And the variant obligation makes non-divergence of newly introduced events a proof obligation rather than an assumption, so a refinement cannot smuggle in an event that runs forever. Liveness is not implied by refinement and needs its own obligations, supplied by Hoang and Abrial (2011).

Applies to. Distributed systems. Protocols. Reactive systems. Industrial verification.

Limitations. What refinement preserves is safety. A discharged refinement chain says invariants hold and new events converge; it does not entail liveness, fairness, or deadlock freedom, each of which must be stated and proved separately, and deadlock freedom in particular is a disjunction of guards that can fail silently in a refinement that strengthens them. Events are atomic by construction, so the model has no notion of an event in progress and genuinely overlapping behaviour must be encoded as an interleaving; real time is not in the language at all. There is no parallel composition operator with an algebraic theory — machines relate only by refinement and by decomposition patterns — so the compositional reasoning a process algebra supplies is unavailable. The mathematical language is first-order set theory without recursive definitions or a fixpoint operator, so inductive structures are axiomatized in a context and their properties proved rather than obtained, and validity there is undecidable. Convergence variants are natural numbers or finite sets, so termination arguments needing transfinite ordinals cannot be expressed.