eSpark nutzte TLA+, um zu beweisen, dass kein Entwurf alle drei Regeln erfüllte, und gab dann eine davon auf

eSpark Learning, ein Anbieter von Bildungstechnologie für Grundschulen, betrieb für jeden Kunden einen manuellen, halbregelmäßigen Konfigurationsprozess, der mehrere Drittsysteme koordinierte und direkt die IT-Netzwerke der Kunden veränderte. Als die Nutzerbasis wuchs, wurde der Arbeitsaufwand untragbar – das Support-Team erkannte, dass es allein zur Aufrechterhaltung jährlich eine neue Vollzeitkraft einstellen müsste. Die Führungsebene hatte die Automatisierung des Prozesses stets als zu riskant eingestuft: Ein Fehler könnte das Netzwerk eines Kunden betreffen und den Vertrag kosten.

Der Ingenieur Hillel Wayne hatte kurz zuvor bei einem Batch-Uploader-Projekt formale Spezifikation (im TLA+-Stil) eingesetzt und durch das Aufspüren von Architekturfehlern vor dem Schreiben von Code eine Woche bei der Lieferung eingespart. Der Projektmanager hatte drei Eigenschaften definiert, die der automatisierte Ersatz garantieren musste, um sicher zu sein. Wayne modellierte das System in einer Spezifikationssprache und ließ es durch einen Model Checker laufen, der erschöpfend jedes Szenario simuliert, das eine Spezifikation zulässt, und einen konkreten Ablauf zurückgibt, wenn er eines findet, das eine Regel verletzt.

Nach zwei Tagen Modellierung scheiterte jeder Entwurf entweder sofort oder enthielt einen subtilen Fehler, der monatelang unbemerkt in der Produktion bestehen und dann zusammenbrechen konnte. Manche Entwürfe erfüllten zwei der drei geforderten Eigenschaften, aber keiner erfüllte alle drei. Statt trotzdem einen auszuwählen und zu hoffen, brachte Wayne den Projektmanager mit den Modellierungsartefakten zusammen, zeigte konkret, wie jeder Entwurf scheitern würde, und fragte, auf welche Eigenschaft das Unternehmen verzichten könnte.

Interne Designexperten stellten fest, dass eine Eigenschaft nur üblicherweise, nicht immer gelten musste. Nachdem dieser eine Kompromiss eingegrenzt war, bestätigte der Model Checker, dass nun mehrere Entwürfe funktionieren würden, und das Team baute einen davon. Der automatisierte Konfigurationsdienst lief danach jahrelang ohne Zwischenfall und überdauerte die Amtszeit der Ingenieure, die ihn gebaut hatten.

Der Model Checker bewies, dass kein Entwurf alle drei Regeln erfüllte; auf dieser Grundlage wurde verhandelt.

Die Modellierung in einer Spezifikationssprache lässt sich billig verwerfen; eine weitgehend fertiggestellte Codebasis nicht, daher vermied das Testen jeder Entwurfsidee vor der Implementierung verschwendete Ingenieurszeit.

Ein Model Checker liefert einen konkreten Fehlerablauf, der für einen nicht technischen Stakeholder überzeugender ist als eine abstrakte Risikowarnung.

Das Aufzeigen von „Keiner dieser Entwürfe erfüllt alle drei Anforderungen“ vor dem Schreiben von Code verwandelte eine implizite, ungeprüfte Annahme in eine explizite Entscheidung, die der Projektmanager tatsächlich treffen konnte.

Wenn jeder Entwurf, den Sie versuchen, zu scheitern scheint, modellieren Sie den Raum zuerst formal. Ein Model Checker verwandelt ein vages Risikogefühl in einen konkreten, verhandelbaren Kompromiss, den Sie vorbringen können, bevor Code geschrieben wird.

Der automatisierte Konfigurationsverwaltungsdienst lief jahrelang effizient, weit über die Amtszeiten der Ingenieure hinaus, die ihn gebaut hatten. Wayne arbeitete anschließend Vollzeit als Berater für formale Spezifikation und schrieb über die Praxis, darunter ein Buch zu dem Thema und Dokumentationsarbeit für die Spezifikationssprache Alloy.