Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing

Dieser Beitrag stellt eine formale Modellierung, Verifikation und Testung der verteilten Middleware „Contract Automata Runtime Environment" (CARE) mittels des Tools Uppaal vor, um durch die Generierung konkreter Tests aus abstrakten Modellen die Zuverlässigkeit der Anwendung zu erhöhen.

Das Wesentliche

Hier ist eine einfache Erklärung der wissenschaftlichen Arbeit, vorgestellt als eine Geschichte über einen hochkomplexen, aber gut organisierten Orchester-Konzert.

Das große Orchester: Wie man Software-Verträge sicher macht

Stellen Sie sich vor, Sie leiten ein riesiges Orchester. Jeder Musiker (ein Computer-Programm oder "Dienst") spielt sein eigenes Stück. Damit daraus ein harmonisches Konzert wird, müssen sie sich genau absprechen: Wer spielt wann welche Note? Wer gibt das Signal zum Start? Wer hört zu?

In der Welt der Computer nennt man diese Absprachen "Verträge". Das Programm, das diese Verträge verwaltet und dafür sorgt, dass alle Musiker im Takt bleiben, heißt CARE (Contract Automata Runtime Environment). Es ist wie der Dirigent und die Sound-Technik in einem, die sicherstellen, dass kein Musiker falsch einsetzt oder die Musik abbricht.

Das Problem? Auch die besten Dirigenten und die teuerste Technik können Fehler haben. Manchmal passiert es, dass ein Musiker auf das Signal wartet, das nie kommt, und das ganze Orchester erstarrt (ein sogenannter "Deadlock" oder Stillstand). Oder Nachrichten gehen verloren, wie ein Brief, der nie im Briefkasten landet.

Die Herausforderung: Der Dirigent im Labor

Der Autor dieser Arbeit, Davide Basile, hat sich vorgenommen, nicht nur das Orchester zu beobachten, sondern es in einem perfekten, kontrollierten Labor zu testen, bevor es auf die große Bühne geht.

Er hat das CARE-System nicht einfach nur mit dem Auge betrachtet, sondern es in eine mathematische Landkarte übersetzt. Man kann sich das vorstellen wie einen riesigen, interaktiven Videospiele-Code, der genau simuliert, wie das Orchester funktioniert.

Hier sind die drei Hauptakteure in dieser Geschichte:

1. Die Landkarte (Das formale Modell)

Statt den echten, komplizierten Java-Code zu lesen (der wie eine dicke, unübersichtliche Telefonbuch-Liste wirkt), hat der Autor eine vereinfachte, aber präzise Landkarte erstellt.

• Die Analogie: Stellen Sie sich vor, Sie wollen testen, ob ein neues U-Bahn-System sicher ist. Sie bauen nicht erst die ganze U-Bahn, sondern ein perfektes Modell im Maßstab 1:100. Sie können damit testen: "Was passiert, wenn zwei Züge gleichzeitig in denselben Tunnel wollen?"
• In diesem Papier wurde CARE als Netzwerk von stochastischen Zeitautomaten modelliert. Klingt kompliziert? Es bedeutet einfach: Eine Karte, die zeigt, wer wann was tun kann, inklusive Zufallselementen (wie: "Wie lange dauert es, bis eine Nachricht ankommt?").

2. Der Prüfer (Uppaal)

Um diese Landkarte zu testen, benutzte der Autor ein Werkzeug namens Uppaal.

• Die Analogie: Uppaal ist wie ein extrem geduldiger, übermenschlicher Prüfer, der das Orchester Millionen von Malen in Sekundenschnelle durchspielen lässt. Er probiert jede denkbare Kombination aus: "Was, wenn Musiker A träge ist? Was, wenn Musiker B eine Nachricht verpasst? Was, wenn der Dirigent einen Fehler macht?"
• Der Prüfer sucht nach zwei Dingen:
  1. Toten Winkel (Deadlocks): Steht das Orchester jemals still, weil alle warten?
  2. Verlorene Noten (Orphan Messages): Gibt es Nachrichten, die im System herumfliegen und nie jemand empfängt?

Das Tolle an Uppaal ist, dass er nicht nur zufällig herumklickt, sondern mathematisch beweist, dass unter bestimmten Bedingungen niemals ein Fehler auftreten kann.

3. Der Brückenbauer (Test-Generierung)

Das war der geniale Teil der Arbeit: Wie stellt man sicher, dass die Landkarte auch wirklich der Realität entspricht?

• Die Analogie: Oft passiert es, dass man ein perfektes Modell im Labor baut, aber die echte U-Bahn funktioniert anders. Der Autor hat einen Trick angewendet: Er hat aus der Landkarte automatisch Prüf-Skripte generiert, die dann direkt auf den echten Code angewendet wurden.
• Er hat quasi aus dem Modell eine "Schatzsuche" erstellt. Das Modell sagt: "Gehe von Punkt A nach Punkt B, dann nach C." Der Computer nimmt diese Anweisung und wandelt sie in einen echten Test für das Java-Programm um.
• Wenn der Test im echten Programm fehlschlägt, weiß man sofort: "Aha! Unsere Landkarte war nicht genau genug, oder im echten Programm steckt ein Fehler."

Was wurde entdeckt? (Die spannenden Momente)

Dank dieses Prozesses wurden echte Probleme gefunden, die sonst vielleicht unentdeckt geblieben wären:

• Der "Wartezimmer"-Fehler: In einer früheren Version des Codes wartete der Dirigent darauf, dass alle Musiker antworten, auch auf solche, die gar nicht am aktuellen Stück beteiligt waren. Das hätte dazu geführt, dass das Orchester ewig wartet (Deadlock). Der mathematische Prüfer hat das sofort gesehen, weil er alle Szenarien durchspielte.
• Die Puffer-Größe: Wie viele Nachrichten können gleichzeitig in der Warteschlange liegen? Der Autor hat mit dem Modell simuliert, wie groß diese Warteschlangen sein müssen, damit nichts verloren geht, ohne dass das System zu langsam wird.

Warum ist das wichtig?

Normalerweise testen Entwickler Software, indem sie sie einfach laufen lassen und hoffen, dass es klappt. Das ist wie ein Flieger, der ohne Sicherheitscheck fliegt, in der Hoffnung, dass er nicht abstürzt.

Dieser Papier zeigt einen anderen Weg:

1. Modellieren: Erst die perfekte Theorie bauen.
2. Verifizieren: Mathematisch beweisen, dass die Theorie sicher ist.
3. Testen: Die Theorie nutzen, um automatisch Tests für die echte Praxis zu schreiben.

Das Ergebnis ist ein sichereres, zuverlässigeres Software-System. Es ist wie ein Dirigent, der nicht nur gut dirigiert, sondern auch weiß, dass sein Orchester unter jeden Umständen nicht aus dem Takt gerät.

Fazit für den Alltag

Stellen Sie sich vor, Sie bauen ein Haus. Statt nur zu hoffen, dass die Wände stehen, bauen Sie erst ein digitales 3D-Modell, simulieren Erdbeben und Stürme darauf, finden Schwachstellen, reparieren diese im Modell und bauen dann das echte Haus. Wenn Sie fertig sind, nutzen Sie den Bauplan, um automatisch zu prüfen, ob das echte Haus wirklich so gebaut wurde wie geplant.

Genau das hat Davide Basile mit dem CARE-System gemacht. Er hat gezeigt, dass formale Methoden (also mathematische Beweise) nicht nur für theoretische Wissenschaftler sind, sondern echte, fehlerfreie Software für die Welt produzieren können.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing" auf Deutsch.

1. Problemstellung

Das Paper adressiert die Zuverlässigkeit und Korrektheit des Contract Automata Runtime Environment (CARE), einer verteilten Middleware-Anwendung, die auf Java basiert. CARE koordiniert Dienste, die durch Verhaltensverträge (Contract Automata) spezifiziert sind. Während die Algorithmen zur Orchestrierung und Synthese von Verträgen in CARE bereits formal bewiesen wurden, bleibt die Laufzeitumgebung selbst (die niedrigschichtigen Interaktionen zwischen Orchestrator und Diensten über TCP/IP-Sockets) oft unformalisiert.

Das zentrale Problem besteht darin, dass Algorithmen, die mathematisch korrekt sind, in der Implementierung aufgrund von Fehlern in der Kommunikationslogik (z. B. Deadlocks, verlorene Nachrichten, Race Conditions) versagen können. Bisherige Ansätze in der Literatur fehlten oft an einer direkten Verbindung zwischen dem abstrakten Formalmodell und dem tatsächlichen Quellcode, was die Validierung der Abstraktionsebene erschwerte.

2. Methodik

Die Autoren wenden einen Bottom-up-Ansatz an, bei dem ein bestehendes, Open-Source-System (CARE) formal modelliert und analysiert wird.

• Formale Modellierung:

  • Das System wird als Netzwerk von stochastischen zeitgesteuerten Automaten (Stochastic Timed Automata) modelliert, kompatibel mit dem Tool Uppaal.
  • Abstraktion: Unwesentliche Details (z. B. der spezifische Inhalt der Nutzdaten/Payloads) werden abstrahiert. Stattdessen werden probabilistische Entscheidungen für Aktionen und Übergänge verwendet, um die Gültigkeit für jede mögliche Orchestrierung zu gewährleisten.
  • Kommunikation: Java TCP/IP-Sockets werden durch globale FIFO-Arrays (Warteschlangen) modelliert. Das Modell berücksichtigt blockierende Lese-/Schreibvorgänge und implementiert einen SocketTimeout-Automaten, um Zeitüberschreitungen zu simulieren.
  • Konfigurationen: Das Modell unterstützt verschiedene Konfigurationen für die Auswahl von Übergängen (diktatorisch vs. mehrheitsbasiert) und die Ausführung von Aktionen (zentralisiert vs. verteilt).

• Verifikation:

  • Es werden sowohl exhaustive Model Checking (erschöpfende Prüfung) als auch Statistical Model Checking (SMC) eingesetzt.
  • SMC wird genutzt, um das System bei größeren Parametereinstellungen (mehr Dienste, größere Puffer) zu skalieren und quantitative Eigenschaften (Wahrscheinlichkeiten) zu ermitteln.
  • Exhaustives Checking wird für kleinere Konfigurationen genutzt, um absolute Garantien (z. B. Abwesenheit von Deadlocks) zu beweisen.

• Traceability und Testing:

  • Ein entscheidender Aspekt ist die Traceability: Jeder Übergang im Uppaal-Modell ist durch Kommentare direkt mit den Zeilen des Java-Quellcodes verknüpft.
  • Modellbasiertes Testen (MBT): Aus den Uppaal-Modellen werden abstrakte Testfälle generiert (mittels Yggdrasil). Diese werden durch Hinzufügen konkreter Daten und Assertions in JUnit-Tests für die CARE-Implementierung überführt.

3. Wichtige Beiträge

1. Formales Modell von CARE: Die erste Bottom-up-Formalisierung einer etablierten Open-Source-Distributed-Middleware als Netzwerk stochastischer zeitgesteuerter Automaten.
2. Verifikationseigenschaften: Nachweis wichtiger Eigenschaften wie:
   • Abwesenheit von Deadlocks.
   • Abwesenheit von „verwaisten" Nachrichten (Orphan Messages) bei Beendigung.
   • Korrekte Terminierung aller Dienste bei Beendigung des Orchestrators.
   • Erkennung von Konfigurationsinkonsistenzen zwischen Orchestrator und Diensten.
3. Verbindung von Modell und Code: Etablierung einer direkten Spurbarkeit zwischen dem abstrakten Modell und dem Quellcode. Dies ermöglicht die Validierung der gewählten Abstraktionsebene.
4. Generierung konkreter Tests: Demonstration eines vollständigen Workflows, bei dem abstrakte Pfade aus Uppaal in lauffähige JUnit-Tests für die reale Anwendung transformiert werden.
5. Fehlererkennung: Identifikation und Behebung von Fehlern in der Implementierung, die durch reines Testen schwer zu finden waren (z. B. ein Deadlock-Szenario, bei dem der Orchestrator auf Antworten von nicht beteiligten Diensten wartete).

4. Ergebnisse

• Verifikationserfolg: Das Modell wurde erfolgreich gegen die definierten Eigenschaften verifiziert.
  • Statistische Ergebnisse: Die Wahrscheinlichkeit von Timeouts oder verbleibenden Nachrichten in den Puffern bei Beendigung wurde als nahe null bestätigt (Konfidenzintervall 0,95 bzw. 0,995).
  • Exhaustive Ergebnisse: Für kleinere Konfigurationen (4-5 Dienste, Puffergröße 3-5) wurde die Abwesenheit von Deadlocks und die korrekte Terminierung mathematisch bewiesen.
• Fehlerbehebung: Während des Modellierungsprozesses wurde ein kritischer Fehler in der Implementierung entdeckt: Der Orchestrator wartete fälschlicherweise auf Antworten von Diensten, die an einer Wahl nicht beteiligt waren, was zu einem Deadlock führte. Dieser wurde durch die Analyse des Gegenbeispiels (Counterexample) in Uppaal gefunden und behoben.
• Testabdeckung: Die generierten JUnit-Tests decken einen signifikanten Teil des Quellcodes ab (Visualisierung durch IntelliJ Coverage), was bestätigt, dass das Modell nicht zu stark abstrahiert ist.
• Parametertuning: Durch SMC konnten optimale Parameter für Puffergrößen und Timeout-Werte im Modell ermittelt werden, die das reale Verhalten gut abbilden, ohne den Zustandsraum unnötig zu vergrößern.

5. Bedeutung und Ausblick

Dieses Paper demonstriert die praktische Anwendbarkeit formaler Methoden in der Softwareentwicklung bestehender Systeme. Es überwindet die Lücke zwischen theoretischer Verifikation und praktischer Implementierung, indem es Open-Source-Code direkt mit formalen Modellen verknüpft.

• Zuverlässigkeit: Die Arbeit erhöht das Vertrauen in die Zuverlässigkeit von CARE durch formale Garantien, die über reine Testabdeckung hinausgehen.
• Reproduzierbarkeit: Alle Modelle, Formeln, Logs und Tests sind öffentlich verfügbar, was eine hohe Reproduzierbarkeit und Nachvollziehbarkeit ermöglicht.
• Zukunftsausblick: Die Autoren planen, die manuelle Synchronisation von Modell und Code zu automatisieren und neue Tools (wie Uppex) zu nutzen, um die Zusammenarbeit zwischen Softwareentwicklern und Modellierern zu erleichtern.

Zusammenfassend liefert das Paper einen robusten Nachweis dafür, dass formale Modellierung, Verifikation und modellbasiertes Testen effektiv eingesetzt werden können, um die Zuverlässigkeit komplexer verteilter Middleware-Systeme zu erhöhen und versteckte Implementierungsfehler aufzudecken.