Lab für formale Methoden: Z3, SPIN, TLA+ und Alloy in einer VM

Dieses Lab gibt jeder Person vier Verifikationswerkzeuge in einer Ubuntu-VM. Testen zeigt, dass ein Entwurf in den ausprobierten Fällen funktioniert. Eine formale Methode lässt eine Maschine alle Fälle ansehen und entweder die Eigenschaft beweisen oder ein Gegenbeispiel liefern. Die Lernenden nutzen Z3, einen Solver, SPIN, einen Modellprüfer für Promela, TLA+ mit seinem Prüfer TLC und Alloy, jedes an einem kleinen Problem.

Auf dem Rechner der Lernenden wird nichts installiert. Die Werkzeuge sind die echten, und die README des Labs nennt die Probleme und keine Lösung.

Was die Lernenden lernen

Was es heißt, einen Entwurf zu prüfen, statt ihn auszuprobieren, in vier Teilen. Mit Z3 formulieren sie die Regeln eines Klausurplans und dann eine Behauptung, die aus den Regeln folgt und die Z3 beweist, indem es zeigt, dass ihr Gegenteil keine Lösung hat. Mit SPIN finden sie in einem Ablauf einen Wettlauf zwischen zwei Prozessen und schreiben dann ein Lock, sodass kein Fehler bleibt. Mit TLA+ schreiben sie die Invariante, die sagt, wozu ein Lock da ist, lesen das Gegenbeispiel, das TLC für ein Lock ausgibt, das nicht sperrt, und beheben es. Mit Alloy lesen sie ein Gegenbeispiel, das als Personen und Freundschaften gezeichnet ist, und reparieren das Modell mit einem neuen Fakt.

Im Browser ausführen

VM-Labs werden als Lab-Aufgabe in einem Modul eingerichtet, und das Beispiel liegt auf der Seite des Labs. Die Maschine ist klein: eine CPU, 1 GB Arbeitsspeicher und 10 GB Festplatte. Jedes Java-Werkzeug ist auf 128 MB begrenzt, und das Ganze passt bequem. Z3 und SPIN brauchen nur das Ubuntu-Archiv. TLA+ und Alloy werden von GitHub geladen, das eine Gast-VM ohne Konto nicht erreicht, deshalb brauchen diese beiden Teile eine angemeldete VM.

  1. Lab hinzufügen. Fügen Sie in einem Modul, das Sie unterrichten, eine Aufgabe hinzu und wählen Sie die Karte Ubuntu-VM-Lab. Die Seite zeigt statt einer Compose-Datei eine kurze Beschreibung der Maschine.
  2. Mit dem Beispiel beginnen. Die Seite bietet fertige Labs zum Einstieg an. Wählen Sie Formal methods. Ein Beispiel ersetzt den Text, und Rückgängig bringt Ihren zurück.
  3. Veröffentlichen und eigene Kopie starten. Veröffentlichen Sie, dann starten Sie. Das Setup-Skript des Labs installiert Z3, SPIN und eine Java-Laufzeit aus dem Ubuntu-Archiv, lädt TLA+ und Alloy aus ihren GitHub-Releases herunter und prüft jede Datei gegen eine feste Prüfsumme, beim ersten Start der VM, in einigen Minuten.
  4. Terminal öffnen. Öffnen Sie das Terminal und lesen Sie README.md im Home-Ordner: Sie sagt, was in vier Teilen zu tun ist, und gibt keine Lösung vor.

Eine Basislektion zu diesem Lab

Formal Methods Basics ist eine kleine Lektion, die in diesem Lab, einer Ubuntu-VM, durchgeführt wird. Sie hat einen Einstieg, ein Ich-kann-Ziel, Schlüsselwörter, einen Starter, nach jeder Idee eine Kontrolle, einen häufigen Fehler und eine Abschlusskontrolle, und jeder Schritt hat eine Schaltfläche Ausführen, die seinen Befehl ins Terminal der Maschine tippt. Die Lernenden stellen Z3 eine Frage, die es beantworten kann, und eine, die es nicht kann, lassen SPIN den Wettlauf im Modell des Labs finden und spielen ihn ab, lesen das Gegenbeispiel, das TLC für eine Invariante ausgibt, die für ein korrektes Lock falsch ist, und sehen eine Alloy-Instanz.

Die Lektion schaut sich nur um und überlässt die eigentlichen Aufgaben des Labs den Lernenden, daher gibt sie keine Lösung vor.

Wie bewertet wird

Das Lab hat eine Prüfung, und sie glaubt den Werkzeugen und nie den Worten der Lernenden. Z3 selbst vergleicht die Regeln des Klausurplans der Lernenden mit denen der README, daher fällt eine von Hand geschriebene Antwort oder eine fehlende Regel durch, und die Behauptung muss aus den Regeln folgen, ohne sie aber nicht gelten. SPIN führt das Lock der Lernenden in einem eigenen Rahmen der Prüfung aus, und das Lock darf nichts nennen, was dem Rahmen gehört. TLC führt das behobene Lock mit der Invariante der Prüfung und der der Lernenden aus, beide Prozesse müssen eintreten können, und die Invariante der Lernenden muss vom mitgelieferten kaputten Lock verletzt werden, sodass eine Invariante TRUE durchfällt. Alloy öffnet das Modell der Lernenden aus einer eigenen Datei mit eigenen Assertions, die gelten müssen, und einem Lauf, der weiterhin eine Gruppe von Freunden finden muss. Die erste Zeile der Ausgabe sagt, warum.

  1. Zuweisen. Weisen Sie das Lab wie jede Aufgabe zu, auf Wunsch mit Abgabetermin. Jede Schülerin und jeder Schüler erhält eine eigene VM, die zwischen den Sitzungen erhalten bleibt, wenn ein Konto besteht.
  2. Prüfung ausführen. Drücken Sie in der Zeile einer Person in der Klassenliste auf Prüfung ausführen. Das startet eine Kopie ihrer gespeicherten Maschine, die nicht zurückgespeichert wird, führt das Prüfskript des Labs als root aus und zeigt, ob es bestanden wurde, was es ausgegeben hat und wann. Die Person erfährt das Ergebnis nicht.
  3. Bewerten. Lesen Sie die erste Zeile der Prüfungsausgabe: Sie nennt den Teil und sagt, was nicht stimmt, etwa eine Regel, die Z3 vermisst, ein Lock, in dem SPIN noch einen Fehler findet, eine Invariante, die das kaputte Lock nicht erkennt, oder ein Modell, das noch ein Gegenbeispiel hat. Geben Sie die Arbeit mit einer Begründung zurück, wenn mehr nötig ist.

Die Definition auf GitHub

Die Datei ist die ganze Lab-Definition, derselbe Text, den die Plattform ausführt: Größe, Setup-Skript, Hilfsbefehle, README und Prüfung. Kopieren Sie sie und ändern Sie die Probleme, um ein längeres Lab zu bauen.

Dieses Lab ausprobieren, und was es kostet

Mit einem kostenlosen persönlichen Konto können Sie die Grundlagenlektionen in diesem Lab durcharbeiten, mit genug kostenlosem Guthaben pro Monat für die meisten Lektionen und ohne Karte. Für eine Klasse sind die ersten 365 Tage für eine Schule kostenlos, für bis zu 50 Lernende; danach zahlt sie je lernender Person und Jahr, alle Labs inklusive und Lehrkräfte kostenlos.

Häufige Fragen

Braucht das Lab eine Lizenz?
Nein. Z3 steht unter MIT, SPIN unter BSD, die TLA+-Werkzeuge unter MIT und Alloy unter Apache 2.0, mit Solvern unter ihren eigenen offenen Lizenzen in seiner jar-Datei. Sie werden beim Start auf der VM der Lernenden installiert, und wir verteilen keines davon.
Kann eine Person ohne Konto es machen?
Teil eins und zwei, Z3 und SPIN, ja. Eine VM ohne Konto erreicht nur das Ubuntu-Archiv, daher sind TLA+ und Alloy dort nicht ladbar. Die VM einer angemeldeten Person erreicht GitHub und bekommt alle vier.
Können Lernende etwas kaputt machen?
Nur ihre eigene Kopie. Die Werkzeuge prüfen Modelle und führen nichts von anderen aus. Wenn jemand eine Datei zerstört, liegt die Originalkopie in /usr/share/formallab.
Wurde das Lab in einer echten Schüler-VM getestet?
Setup, die Befehle der Lektion und die Prüfung liefen in einem echten Ubuntu 26.04 in einem Container, der die VM vertrat, und die Prüfung fiel bei jeder Art, jeden Teil zu schummeln, durch und bestand mit der Referenzlösung. Eine wirklich gestartete Schüler-VM und der Download über den Proxy der Plattform sind einen Versuch vor dem Unterricht wert.