Die B-Methode ist eine formale Methode zur systematischen Entwicklung von Software: Aus einer mathematischen Spezifikation wird Schritt für Schritt eine implementierbare Maschine abgeleitet, wobei jeder Schritt mit automatisch erzeugten Beweisverpflichtungen (Proof Obligations) abgesichert wird. Entwickelt wurde sie von Jean-Raymond Abrial, dem Mitentwickler der Z-Notation, ab Ende der 1980er-Jahre.
Maschinen, Verfeinerung und Beweis
Ein B-Modell besteht aus Komponenten: MACHINE (abstrakte Spezifikation), REFINEMENT (Verfeinerungsschritt) und IMPLEMENTATION (ausführbare B0-Variante). Eine Maschine definiert Zustandsvariablen, eine Invariante (immer gültige Eigenschaft) und Operationen. Jede Verfeinerung erzeugt Beweisverpflichtungen: Ist die Invariante erhalten? Verfeinert die neue Operation die abstrakte korrekt? Sind alle Beweise geführt, garantiert die Methode, dass die finale B0-Spezifikation die ursprüngliche Anforderung korrekt umsetzt.
Werkzeuge und Befehle
atelierb # GUI-Start von Atelier B (CLEARSY)
pogen # Proof-Obligation-Generator
prover # Beweis-Manager (interaktive Beweise)
obcomp # B0-Compiler zu Ada/C
probcli -model_check # ProB: Model Checking eines B-Modells
probcli -ltlcheck # ProB: LTL-Eigenschaften pruefen
prob -repl # ProB: interaktive REPLAtelier B wurde ab 1995 von CLEARSY industrialisiert. Das bekannteste Projekt ist die Pariser Metrolinie 14 (Météor): Der Vertrag ging 1995 an Matra Transport (heute Siemens), das Modell umfasste rund 110.000 Zeilen B-Code, wurde 1998 fertiggestellt und fuhr ohne einen einzigen softwarebedingten Fehler — ein Meilenstein der formalen Verifikation in der Praxis. Auch die automatische Metro Roissy VAL (CDGVAL) am Flughafen Charles de Gaulle wurde mit B entwickelt. ProB von Michael Leuschel ergänzt die Deduktion durch Animation und Model Checking.
Einordnung
Die B-Methode ist eng mit VDM und der Z-Notation verwandt; ihre Weiterentwicklung für reaktive Systeme ist Event-B. Zur selben Werkzeugfamilie gehören TLA+, Isabelle und ACSL/Frama-C.
Verwandte Grundlagen: C/C++-Befehle (Zielsprache der B0-Codegenerierung), Prolog-Befehle (Logikprogrammierung als Verifikationsnachbar).