Event-B

Origin. Jean-Raymond Abrial (2000s). Evolution of B. Event-driven. Reactive systems. Foundation of Rodin platform.

Models. Machines with events. Not operation calls but events. Refinement methodology. Proof-based development. System-level modeling.

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. THEN: action. ANY: local parameters. WITNESS: refinement witness.

Proof obligations: INV: events preserve invariant. FIS: events feasible. GRD: guard strengthening. SIM: simulation.

Refinement patterns: Data refinement. Event splitting. Event merging. New events (convergent/anticipated).

Convergence: VARIANT V (natural number expression). New events must decrease V. No infinite new-event sequences. Ensures progress.

Rodin platform: Eclipse-based IDE. Proof obligation generation. Interactive/automatic proving. Animation, model checking.

Symbols.

Metatheory. Event-driven. Refinement. Proof obligations. Reactive systems.

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

Limitations. No process algebra. Proof effort. Learning curve. Tool dependency.