eventb-rossi/eventb-skill

Entwickeln von Event-B-Modellen

Ein Event-B-Modell ist ein diskretes Transitionssystem. Ein CONTEXT enthält feste Mengen, Konstanten und Axiome; eine MACHINE enthält Variablen, Invarianten und bewachte Ereignisse. Diese Fähigkeit überprüft erreichbares Verhalten mit ProB und prüft die Wohldefiniertheit. Sie erstellt keine interaktiven Rodin-Beweise.

1. Überprüfen der erforderlichen Werkzeuge

Erforderlich sind rossi 0.1.8+ und eventb-animate 6.4+. Überprüfen Sie diese; installieren oder aktualisieren Sie sie niemals selbst. Wenn eines fehlt oder älter ist, stoppen Sie und bitten Sie den Benutzer, dies zu tun.

command -v rossi eventb-animate
rossi --version
eventb-animate --version

2. Umfang vor der Modellierung

Schreiben Sie ein kurzes Anforderungsblatt in der README.md des Modells:

• Systemgrenze und explizite Ausnahmen;
• beobachtbare Ereignisse und wer sie ausführt;
• Zustandstypen und die Sicherheitseigenschaften, die immer gelten müssen;
• ein erreichbares Erfolgsszenario, ein wichtiges verbotenes Szenario und ob ein Endzustand beabsichtigt ist.

Für ein umfangreiches Modell oder eine mehrstufige Verfeinerung fügen Sie eine Anforderungs-zu-Verfeinerungs-Tabelle mit einer Zeile pro Stufe hinzu: Anforderungs-/Standardklausel, neuer oder ersetzter Zustand, betroffene Ereignisse, Invariante/Verklebungsbeziehung und Validierungsfrage. Teilen Sie eine Stufe, deren Zeile nicht zusammenhängende Belange enthält.

Verwenden Sie standardmäßig eine Maschine; teilen Sie feste Daten in so viele kleine Kontexte auf, wie es ihre unabhängigen Belange erfordern. Fügen Sie nur dann eine Verfeinerungsstufe hinzu, wenn sie eine bestimmte Anforderung isoliert oder eine Datenrepräsentation ersetzt; schreiben Sie zuerst diesen Grund und die Verklebungsinvariante. Verfeinerung ist ein Werkzeug, keine erforderliche Zeremonie.

Halten Sie jedes Modell in einem eigenen Projektverzeichnis. Verwenden Sie eine Komponente pro Datei, wobei die Datei nach der Komponente benannt ist. Fügen Sie keine Prosa-Kommentare in .eventb-Dateien ein; bewahren Sie die Erklärung in der README.md.

3. Nur die relevante Referenz lesen

Bedarf	Lesen
Exakte .eventb-Grammatik und Aktionsformen	references/syntax.md
Ein Operator oder seine Priorität	references/math-toolkit.md
Hilfe bei der Wahl von Zustand, Invarianten oder Ereignissen	references/modelling.md
Ein echter Verfeinerungsschritt oder Planung einer Kette	references/refinement.md
Ein grundlegendes Muster für reaktive Systeme	die entsprechende Überschrift in references/patterns.md
Diskrete Zeit, Fristen, Modi oder Sensoren/Aktoren	references/patterns-control.md
Mehrere Teilnehmer: Topologie, Runden, Konsens, Kanäle, langlaufende Operationen	references/patterns-distributed.md
Zugriffskontrolle, Autorisierungsrichtlinie oder Reservierung	references/patterns-security.md
Ableiten einer Schleife aus einer Nachbedingung oder eines Interpreters/ISA	references/patterns-algorithms.md
CLI-Fehlerbehebung oder ein bedingter erweiterter Befehl	references/tooling.md
Abschließende Entwurfsprüfung	references/best-practices.md

Beginnen Sie mit examples/counter/ nur, wenn Zeugen oder Datenverfeinerung beteiligt sind; verwenden Sie examples/cars_on_bridge/ für Ereignisaufteilung/-konvergenz und examples/array_maximum/ für terminierende Algorithmen. Lesen Sie keine Beispiele, nur um ein kleines Ein-Maschinen-Modell zu beginnen.

4. Das kleinste nützliche Modell erstellen

• Platzieren Sie Trägermengen und feste Richtlinien/Konfiguration in einem Kontext.
• Typisieren Sie jede Variable mit ihrer ersten Invariante und geben Sie dann die eigentliche Sicherheitsregel an.
• Wenn Sensorik oder Steuerung eine Systemgrenze überschreitet, halten Sie den physikalischen, gemeldeten und befohlenen Zustand getrennt und geben Sie die zulässige Verzögerung/Unsicherheit zwischen ihnen an.
• Stellen Sie sicher, dass INITIALISATION jede Invariante herstellt.
• Geben Sie jedem Ereignis jede Wächterbedingung, die für die funktionalen und reinen Übergangsanforderungen sowie die Invariantenerhaltung erforderlich ist; Aktionen laufen gleichzeitig ab und nicht zugewiesene Variablen bleiben unverändert.
• Repräsentieren Sie ein wichtiges Ergebnis im Zustand, wenn ein späteres Zustandsziel es beobachten muss. Fügen Sie kein No-Op-Ereignis nur zur Abdeckung hinzu; ein aktiviertes No-Op ändert das Deadlock- und Liveness-Verhalten.
• Halten Sie endliche Prüfszenarien klein. Breite nichtdeterministische Parameter multiplizieren Betriebsaktivierungen und können eine ansonsten endliche Prüfung unvollständig oder langsam machen.

5. Das Kern-Gate ausführen

Führen Sie es aus dem Projektverzeichnis des Modells aus, nicht aus einem übergeordneten Verzeichnis mit nicht zusammenhängenden Modellen. Erstellen Sie eine .zip-Datei; sie enthält die geprüften Dateien, die der Animator benötigt.

rossi fmt -i .
rossi validate .
rossi fmt --check .
rossi build . -o /tmp/model.zip
eventb-animate --json /tmp/model-report.json /tmp/model.zip
eventb-animate wd /tmp/model.zip

Akzeptieren Sie das Ergebnis nur, wenn:

• Validierung und Build keine Fehler haben; behandeln Sie Warnungen wie missing or ill-typed witness und event is inaccurate als Fehler, auch wenn der Befehl mit Null beendet wird;
• der Bericht den Status status: "ok" und keine Invariantenverletzung aufweist;
• es keinen unerwarteten Deadlock gibt; für einen bewussten Endzustand dokumentieren Sie das Endprädikat und führen Sie es erneut mit --no-deadlock aus, anstatt Deadlock-Freiheit zu beanspruchen;
• der menschliche Block Covered operations die erwarteten Ereignisse enthält (Bericht v3 speichert keine Operationsabdeckung, daher erfassen Sie die Befehlsausgabe, wenn dies geprüft werden muss);
• completion.classification für ein endliches Akzeptanzszenario complete ist;
• jede Wohldefiniertheitsverpflichtung erfüllt ist.

Ein Exit-Code von Null ist kein Beweis für Vollständigkeit. Wenn ein endliches Modell als unvollständig gemeldet wird, überprüfen Sie den Grund und die relevanten ProB-Grenzen:

eventb-animate info --prefs /tmp/model.zip \
  | rg 'MAX_(INITIALISATIONS|OPERATIONS)|DEFAULT_SETSIZE'

Erhöhen Sie MAX_INITIALISATIONS oder MAX_OPERATIONS nur so weit, dass die bekannten endlichen Auswahlmöglichkeiten aufgezählt werden, führen Sie es dann erneut aus und fordern Sie completion.classification: "complete". Melden Sie für ein absichtlich generisches/unbeschränktes Modell das beschränkte Ergebnis ehrlich und fügen Sie ein separates kleines endliches Szenario hinzu, wenn eine erschöpfende Prüfung wichtig ist.

Wenn es eine Verfeinerungskette gibt, wiederholen Sie die Modellprüfung und wd für jede Stufe mit -m <machine>.

6. Gezielte Beweise hinzufügen, wenn sie eine Frage beantworten

Verwenden Sie eine Zielablaufverfolgung, wenn die Frage ist, ob ein Zustandsprädikat erreichbar ist:

eventb-animate -m M --goal '<predicate>' --no-invariant --no-deadlock \
  --save /tmp/scenario.json /tmp/model.zip
eventb-animate replay -m M -t /tmp/scenario.json /tmp/model.zip

Ein erreichtes Ziel beendet sich absichtlich mit Exit 1; fordern Sie eine PERFECT-Wiedergabe. Speichern und wiederholen Sie bei einem Invarianten- oder Deadlock-Fehler dessen Gegenbeispiel, bevor Sie das Modell ändern.

Ein Zustandsziel kann nicht beweisen, dass ein aktionsloses oder reines Wächter-Ereignis ausgelöst wurde: Es kann anhalten, sobald der ermöglichende Zustand erreicht ist. Bestätigen Sie einen bestimmten Übergang durch den Block Covered operations der vollständigen Prüfung oder zielen Sie mit der Testgenerierung darauf ab:

eventb-animate testgen -m M --operations EVENT_NAME \
  --out /tmp/scenario-traces /tmp/model.zip

Verwenden Sie diese nur, wenn ihr spezifischerer Zweck zutrifft:

• testgen: Zeuge eines bestimmten Übergangs oder Erstellung wiederverwendbarer Operations-Fixtures; es ist kein stärkeres Gate als eine erschöpfende Prüfung, und "uncovered" ist nicht schlüssig.
• --symbolic ic3|kinduction: Unbeschränkte Invariantensicherheit; es prüft keine Deadlocks, meldet keine Ereignisabdeckung oder liefert Ablaufverfolgungen.
• po: Überprüfen eines vorhandenen Rodin-Projekts, das bereits .bpo/.bps-Beweise enthält.
• import/export: Rodin-Austausch, nicht der normale Autorenzyklus.

Siehe references/tooling.md für diese bedingten Workflows. Das Standard-ProB-Backend ist der normale Autorenpfad.

7. Mit einem lesbaren Artefakt abschließen

Liefern Sie die .eventb-Dateien plus eine kurze README.md mit Umfang, Modellform, der Sicherheitsinvariante in einfacher Sprache, etwaiger Verfeinerungstabelle, genauen Prüfbefehlen, Vollständigkeit, Ereignisabdeckung, WD-Ergebnis und etwaiger bewusster Abstraktion. Ein sauberer beschränkter Durchlauf bedeutet "kein Fehler innerhalb der Grenze gefunden." Ein vollständiger endlicher Durchlauf beweist nur das geprüfte erreichbare Verhalten: Er kann dennoch eine zu starke, nicht-induktive Invariante akzeptieren, weil verletzende Zustände unerreichbar sind. Es erfüllt keine Event-B-Invarianten-/Verfeinerungs-Beweisverpflichtungen; nur ein anwendbares Beweis-Gate unterstützt diese Behauptung. Siehe references/refinement.md, "Model-Checking ist kein Beweis."