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 + SMT

Einordnung

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).

NuSMV (New Symbolic Model Verifier) ist ein weit verbreiteter symbolischer Model Checker, entwickelt an der Universität Trient (FBK-IRST). Er ist die Neuimplementierung und Erweiterung des klassischen SMV von Ken McMillan (CMU), der 1998 den Turing Award für das symbolische Model Checking mit BDDs mitprägte. NuSMV prüft Eigenschaften, die in CTL (Computation Tree Logic) oder LTL (Linear Temporal Logic) formuliert sind, gegen ein endliches Zustandsmodell.

SMV-Eingabesprache

MODULE main
VAR state : {idle, busy};
ASSIGN
  init(state) := idle;
  next(state) := case
    state = idle : busy;
    TRUE        : idle;
  esac;
SPEC AG (state != busy -> AX state = busy)

Eine SMV-Datei beschreibt MODULEs, VAR-Deklarationen, INIT/ASSIGN/TRANS-Übergänge und SPEC-Eigenschaften. Typische CTL-Operatoren sind AG, EG, AF, EF, AX, EX; LTL nutzt G, F, X, U.

Befehle

nusmv modell.smv          # Batch-Modus: Modell laden und alle SPEC pruefen
nusmv -dcx modell.smv     # Dynamic Cone of Influence (Reduktion)
nusmv -p "AG (x = 1)" modell.smv   # Eigenschaft direkt pruefen
nusmv -bmc -k 10 modell.smv        # Bounded Model Checking
# interaktive Session:
read_model                 # Datei laden
go                         # BDD bauen
check_ctlspec              # CTL-Spezifikationen pruefen
check_ltlspec              # LTL-Spezifikationen pruefen
check_invar                # Invarianten pruefen
pick_state; simulate       # Zustand waehlen und Pfade simulieren
print_reachable_states     # erreichbare Zustaende anzeigen
show_vars                  # Variablen auflisten

Die Eigenschaften können entweder in der SMV-Datei stehen oder per -p bzw. über den Property-Index (-n) in der interaktiven Session geprüft werden. -bmc aktiviert das beschränkte Modellprüfen, das mit SAT-Solvern längere Pfade skaliert als die reine BDD-Suche.

Einordnung

Der Nachfolger nuXmv erweitert NuSMV um IC3/PDR-basierte Algorithmen und wird ebenfalls von FBK entwickelt. NuSMV bildet mit SPIN/Promela das Standard-Duo der automatisierbaren Model Checker: SPIN prüft asynchrone Prozesse, NuSMV synchrone endliche Systeme. Zusammen mit TLA+, B-Methode und Event-B deckt er die automatisierte Seite der formalen Verifikation ab.

Verwandte Grundlagen: Z-Notation (Spezifikationssprache), C/C++-Befehle (typische Zielsysteme).

Nemerle ist eine allgemeine, hochsprachliche, statisch typisierte Programmiersprache für die .NET-Plattform, die an der Universität Wrocław (Polen) ab etwa 2003 entwickelt wurde. Sie vereint funktionale, objektorientierte, imperative, aspektorientierte und reflektive Programmierung in einer Sprache und ist besonders für ihre leistungsfähige Makro-Technik bekannt.

Compiler und erste Schritte

Der Compiler heißt ncc und erzeugt Common Intermediate Language (CIL), wodurch volle Kompatibilität mit .NET und Mono entsteht. Ein klassisches Beispiel:

def Main() : void
    System.Console.WriteLine("Hallo, Nemerle!")

Dank starker Typhinferenz sind Typdeklarationen meist überflüssig — der Compiler leitet die Typen aus dem Kontext ab.

Kernkonzepte

• Makros: Das Herzstück von Nemerle. Makros arbeiten auf dem Syntaxbaum und erweitern die Sprache selbst — etwa eigene Kontrollstrukturen oder DSLs, die wie eingebaute Konstrukte aussehen.
• Funktionale Mittel: Pattern Matching (wie in ML/OCaml), unveränderliche Datenstrukturen und Funktionen höherer Ordnung.
• Objektorientiert: Klassen, Vererbung und Interfaces wie in C#.
• Computation Expressions: Ähnlich wie in F# lassen sich Monaden-artige Abläufe definieren.
• XML-Literale: XML lässt sich direkt im Quellcode schreiben und per LINQ abfragen.

Praxis-Tipps

• Nemerle eignet sich für Compiler-Bau und Sprachwerkzeuge, weil Makros die Syntax erweitern können, ohne einen externen Präprozessor zu benötigen.
• Die Sprache gilt als mächtiger als C# und F#, hat aber nur eine kleine Community.
• Einsteiger mit F#- oder OCaml-Hintergrund finden die funktionalen Teile schnell vertraut.

Verwandte Grundlagen: C#-Befehle, F#-Befehle, Scala-Befehle, Compiler sowie die .NET-Alternativsprachen Boo-Befehle und Cobra-Befehle.

Cobra ist eine imperative, hochsprachliche, objektorientierte Programmiersprache, die Charles Esterbrook entworfen hat. Die erste Version erschien 2006, die öffentliche Veröffentlichung unter der MIT-Lizenz folgte 2008. Cobra läuft auf .NET und Mono und kombiniert Python-artige Einrückung mit statischer Typisierung, Design-by-Contract und eingebauten Unit-Tests.

Compiler und erste Schritte

Der Cobra-Compiler übersetzt Quellcode in C# und kompiliert diesen dann mit dem .NET-Compiler weiter. Ein Hallo-Welt-Programm:

class Hallo
    def main
        print 'Hallo, Cobra!'

Cobra nutzt Einrückung statt Klammern, verlangt aber Typangaben für Parameter und Rückgabetypen.

Kernkonzepte

• Design-by-Contract: Aus Eiffel übernommen — Methoden deklarieren Vorbedingungen (require), Nachbedingungen (ensure) und Klasseninvarianten (invariant), die zur Laufzeit geprüft werden.
• Statische und dynamische Typisierung: Standardmäßig statisch, einzelne Variablen können mit dynamic zur Laufzeit aufgelöst werden.
• Eingebaute Unit-Tests: Testfälle stehen direkt im Quellcode — test-Blöcke innerhalb von Klassen werden beim Kompilieren ausgeführt.
• Nil-Tracking: Der Compiler verfolgt zur Compile-Zeit, ob Variablen nil (null) sein können, und verhindert so viele NullReference-Fehler.
• Einfluss von Objective-C: Benannte Parameter und Methoden-Signaturen erinnern an Objective-C-Stil.

Praxis-Tipps

• Die Contract-Prüfung macht Cobra interessant für sicherheitskritische Anwendungen, bei denen Zusicherungen dokumentiert und erzwungen werden sollen.
• Das Projekt ist seit etwa 2015 inaktiv; die Website cobra-language.com ist offline, der Quellcode aber weiterhin verfügbar.
• Für Python-Entwickler ist die Einrückung vertraut; die Typannotationen ähneln C#.

Verwandte Grundlagen: Python-Befehle, C#-Befehle, Eiffel-Befehle, Compiler sowie die .NET-Alternativsprachen Boo-Befehle und Nemerle-Befehle.