Event-B ist die Weiterentwicklung der B-Methode für reaktive, nebenläufige und verteilte Systeme. Jean-Raymond Abrial entwickelte sie in den 2000er-Jahren zusammen mit der Rodin-Plattform, einer Open-Source-IDE auf Eclipse-Basis. Statt Operationen stehen hier Ereignisse (Events) im Mittelpunkt — sie eignen sich dadurch besonders für Systeme, die auf Umgebungsreize reagieren, wie Protokolle, Eisenbahnsicherung oder Blockchain-Konsens.
Modellierungssprache
Ein Event-B-Modell trennt Maschinen (dynamischer Teil) und Kontexte (statischer Teil mit Mengen und Konstanten). Eine Maschine deklariert Variablen, eine Invariante und Events. Jedes Event besteht aus Wachen (grd, Guards: Bedingungen, wann es feuern darf) und Aktionen (act, die die Variablen ändern). Die zugrunde liegende Mathematik ist Mengenlehre und Prädikatenlogik — dieselbe Basis wie die Z-Notation.
Verfeinerung und Beweisverpflichtungen
Das Herzstück ist die schrittweise Verfeinerung: Abstrakte Events werden in konkretere zerlegt, dabei entstehen automatisch Beweisverpflichtungen — Invariantenerhalt, Guard-Verschärfung und Simulationstreue. Die Rodin-Plattform erzeugt diese Proof Obligations und bietet automatische und interaktive Beweisführung (u. a. über SMT-Löser), Animation und Model Checking über das ProB-Plugin.
rodin # Rodin-Plattform starten (Eclipse-basiert)
# Modellkomponenten: .bum (Maschine), .buc (Kontext)
# Events: event name, grd1: ..., act1: ...
# Proof Obligations: automatisch nach Speichern; Auto-Prover + SMTEinordnung
Event-B wird industriell und in der Forschung eingesetzt, etwa zur Verifikation von Blockchain-Konsensmechanismen und Sicherheitsprotokollen. Es ergänzt klassische Model Checker wie NuSMV und SPIN um deduktive Verifikation und ist eng mit Z-Notation, VDM und Alloy verwandt.
Verwandte Grundlagen: Python-Befehle (ProB/Modell-Automation), TLA+ (Alternativ-Ansatz für reaktive Systeme).