Schnittstellen mit Verhaltensvertrag: Protocol State Machines in der Praxis

Viele schwer auffindbare Integrationsfehler haben dieselbe Ursache: Missverständnisse über die tatsächlich erlaubten Ereignis-Reihenfolgen an den Schnittstellen zwischen Komponenten, Subsystemen oder Organisationen. Beschrieben wird dieses dynamische Verhalten meist nur in der begleitenden Dokumentation, als Klartext oder mit Sequenzdiagrammen. Beides hat erhebliche Nachteile: Klartext kann von Werkzeugen nicht ausgewertet werden, und Sequenzdiagramme zeigen nur einzelne Beispiele erlaubten oder verbotenen Verhaltens. In diesem Artikel wird eine Methodik vorgestellt, die das dynamische Verhalten zum formalen Bestandteil des Schnittstellenvertrags macht: die Spezifikation von Protocol State Machines.

Schnittstellen und IDLs: unverzichtbar, aber statisch

In jeder Art von Softwarearchitektur sind Schnittstellen zwischen Komponenten, Subsystemen oder Systemen wichtige Artefakte. Sie repräsentieren den Vertrag nicht nur zwischen diesen Architekturbausteinen, sondern auch zwischen organisatorischen Einheiten wie Teams, Abteilungen oder Unternehmen. Daher werden Schnittstellen häufig als erstklassige Entitäten mit einer Interface Definition Language (kurz: IDL) modelliert. Im Vergleich zu Schnittstellen, die mit einer allgemeinen Programmiersprache definiert werden, sind IDL-Modelle technologieneutral: Dieselbe Definition kann auf einen RESTful-Service abgebildet oder in C++-Code für ein eingebettetes System generiert werden.

Die Landschaft der IDLs hat sich seit den 2010er-Jahren deutlich verbreitert. Für Service-zu-Service-Kommunikation dominiert heute Protocol Buffers mit gRPC, REST-APIs werden mit OpenAPI beschrieben, ereignisbasierte Systeme mit AsyncAPI. Mit TypeSpec (Microsoft) und Smithy (AWS) sind zudem Design-Sprachen entstanden, die aus einer Definition mehrere dieser Formate erzeugen können.

Allen gemeinsam ist der Fokus auf die statischen Aspekte einer Schnittstelle, d.h. Datentypen, Attribute und Operationen. Oft gibt es jedoch Einschränkungen bezüglich der Reihenfolge der Interaktionen auf dem Interface. So muss z.B. eine init()-Methode aufgerufen werden, bevor andere Interaktionen erlaubt sind. Diese Eigenschaft kann keine der genannten IDLs ausdrücken; selbst AsyncAPI beschreibt nur, welche Nachrichten es gibt, nicht deren erlaubte Reihenfolge.

Die Methode: Verhaltensverträge mit Protocol State Machines

Die vertragsbasierte Schnittstellenentwicklung erweitert den Vertrag um eine Verhaltensdimension: Für jedes Interface wird eine Protocol State Machine (kurz: PSM) definiert. Sie legt exakt fest, welche Reihenfolge von Ereignissen bei jeder Implementierung dieses Interfaces erlaubt ist. Jede Sequenz, die von der PSM nicht abgedeckt wird, verletzt den Vertrag. Das Konzept stammt aus der UML, wo Protocol State Machines seit langem Teil des Standards sind; in der Praxis werden sie dort allerdings selten genutzt.

Eine formal definierte PSM läßt sich mit Tools automatisiert auswerten. Dadurch ergeben sich mehrere Nutzungsszenarien:

• Statische Prüfung: Implementierungen und Clients können gegen die PSM verifiziert werden, z.B. durch Model Checking. Protokollverletzungen werden so bereits vor der Integration erkannt.
• Laufzeit-Monitoring: Aus der PSM lässt sich ein Monitor generieren, der Vertragsverletzungen im laufenden System sofort meldet.
• Trace-Validierung: Aufgezeichnete Nachrichten eines realen Systems werden nachträglich gegen die PSM geprüft. Da die Nachrichten zwischen Komponenten oft ohne Änderung des Quellcodes aufgezeichnet werden können (z.B. durch eine Probe in der Kommunikationsinfrastruktur), ist dies ein leichtgewichtiger, aber leistungsstarker Weg zur Validierung der dynamischen Interaktionen.
• Test-Generierung: Aus Interface-Definition und PSM lassen sich Mock-Server und Test-Clients generieren, mit denen ein Interface sofort ausprobiert werden kann.

Die Definition von PSMs bedeutet zwar zusätzlichen Aufwand; nach unserer Erfahrung kostet ein spät gefundener Integrationsfehler jedoch deutlich mehr.

Beispiel: ein Musicplayer-Interface mit Franca IDL

Wie sich diese Methodik in einer IDL umsetzen lässt, zeigt Franca IDL — eine der wenigen IDLs, die Protocol State Machines als festen Sprachbestandteil unterstützen. Franca wurde 2011 vom Autor dieses Beitrags bei der GENIVI Alliance (heute COVESA) initiiert, um Schnittstellen für Infotainment-Plattformen im Fahrzeug zu standardisieren. Das Eclipse-basierte Kernprojekt wird inzwischen nicht mehr aktiv weiterentwickelt; der darauf aufbauende Codegenerator CommonAPI C++ ist bei Fahrzeugherstellern und Zulieferern jedoch weiterhin im Einsatz.

Der folgende Screenshot zeigt ein Beispiel-Interface mit Franca IDL. Es spezifiziert eine einfache Musik-Wiedergabe-API.

Die Methode findTrackByTitle wählt einen Musiktitel anhand eines Eingabe-Strings aus. Von allen passenden Titeln wird der beste Treffer als Attribut currentTrack gesetzt; kann kein Titel gefunden werden, gibt der Server einen NOT_FOUND-Fehlercode zurück. Nachdem ein Titel ausgewählt wurde, steuern die Methoden play und pause die Wiedergabe. Alle Details zu Datentypen und Schnittstellen von Franca IDL sind im Referenzkapitel des Franca User Guide zu finden.

Die folgende PSM spezifiziert das dynamische Verhalten für dieses Interface. Sie legt z.B. fest, dass play nur nach einem erfolgreichen Aufruf von findTrackByTitle aufgerufen werden kann. Der Anfangszustand ist Idle. Zu beachten ist, dass jede Franca-Methode als Call/Respond-Transitionspaar in der PSM dargestellt wird.

Die PSMs werden in Franca IDL in textueller Form direkt bei der Interface-Definition notiert. Damit ist der Verhaltensvertrag Teil desselben Artefakts wie Datentypen und Methoden und kann von allen Werkzeugen der Toolchain ausgewertet werden. Eine solche Toolintegration zwischen Franca IDL und itemis CREATE ist im Blog-Beitrag „Zustandsautomaten-Origami“ beschrieben. Dabei wird die Kommunikation von Verhaltens-Zustandsautomaten mittels Franca-PSMs überprüft.

Die Methodik heute: drei Vertreter

Auch wenn die Mainstream-IDLs Verhaltensverträge bis heute nicht unterstützen, ist die Methodik selbst lebendig. Drei Vertreter zeigen dies:

• Dezyne: Die Sprache Dezyne von Verum (seit 2021 Open Source) spezifiziert Interfaces mit Verhaltensverträgen als Zustandsmaschinen und verifiziert Komponenten per Model Checking. Protokollverletzungen werden so bereits statisch ausgeschlossen, statt zur Laufzeit behandelt zu werden. Zielgruppe sind eingebettete Systeme bei Herstellern von High-Tech-Equipment, bei denen die Kosten mangelnder Qualität hoch sind; im Serieneinsatz ist Dezyne u.a. bei Philips und ASML. Das Ökosystem um die Sprache ist allerdings eine Nische geblieben.
• P: Die bei Microsoft entstandene und heute von AWS weiterentwickelte Sprache P modelliert verteilte Systeme als kommunizierende State Machines. AWS setzt P u.a. bei S3 und DynamoDB ein; mit dem Werkzeug PObserve werden dort Produktions-Logs nachträglich gegen die formale Spezifikation validiert — die oben beschriebene Trace-Validierung im großen Maßstab.
• Session Types: Aus der Forschung stammen Multiparty Session Types und die Protokollsprache Scribble. Ein global definiertes Protokoll wird dabei pro Teilnehmer auf einen endlichen Automaten projiziert, aus dem sich Monitore für die beteiligten Komponenten generieren lassen. Genutzt wird der Ansatz bisher vor allem in Forschung und Pilotprojekten.

Allen drei ist gemeinsam, dass das dynamische Verhalten als formaler Bestandteil des Schnittstellenvertrags behandelt und werkzeuggestützt geprüft wird.

Die Aufwandshürde: PSM-Entwurf mit KI-Unterstützung

Warum also hat sich die Methodik trotz ihrer Vorteile nicht breiter durchgesetzt? Ein wesentlicher Grund ist der Entwurfsaufwand. Eine PSM für ein Interface zu entwerfen erfordert, das dynamische Verhalten vollständig zu durchdenken; viele Entwickler empfinden das als zusätzliche Last neben der eigentlichen Implementierung. Diese Rückmeldung haben wir zwischen 2011 und 2017 bei der Arbeit an Franca im GENIVI-Umfeld immer wieder aus der Praxis erhalten.

Heute gibt es dafür einen neuen Lösungsansatz: leistungsfähige KI-Agenten. Ein Agent kann die vorhandenen Implementierungen einiger Clients und Server analysieren und daraus einen ersten Entwurf der PSM ableiten. Stehen zusätzlich aufgezeichnete Trace-Logs zur Verfügung, lässt sich der Entwurf gegen das tatsächlich beobachtete Verhalten abgleichen. Der Entwickler prüft und verfeinert den Vorschlag anschließend; die Verantwortung für den Vertrag bleibt bei ihm.

Diese Kombination ist deshalb attraktiv, weil sich beide Seiten ergänzen: Der KI-Agent liefert schnell einen Entwurf, und die formale Natur der PSM stellt sicher, dass dieser Entwurf automatisiert überprüfbar bleibt. Fehler des Agenten bleiben damit nicht unentdeckt, sondern werden durch Model Checking oder Trace-Validierung sichtbar. Die Einstiegshürde für die vertragsbasierte Methodik sinkt dadurch deutlich.

Wie man es heute bauen würde

Franca ist eng mit der Eclipse-Plattform verbunden, deren Verbreitung in den letzten Jahren deutlich zurückgegangen ist. Würde man eine IDL mit Protocol State Machines heute neu bauen, sähe der technische Unterbau anders aus: Mit dem Language Server Protocol (kurz: LSP) lässt sich die Sprachunterstützung einmal implementieren und anschließend in VS Code, im Browser oder in anderen Editoren nutzen. Frameworks wie Langium (der Xtext-Nachfolger auf TypeScript-Basis) reduzieren den Aufwand dafür erheblich. Die Prüfung von Traces gegen PSMs würde man heute in die CI-Pipeline integrieren, sodass Vertragsverletzungen bei jedem Testlauf automatisch erkannt werden.

Bei itemis entwickeln wir solche maßgeschneiderten Sprachen und Werkzeuge in Kundenprojekten. Die Methodik der Verhaltensverträge lässt sich dabei in moderne Toolchains ebenso integrieren, wie es Franca seinerzeit in Eclipse vorgemacht hat.

Fazit

Werkzeuge altern, Methoden nicht. Franca IDL hat gezeigt, dass sich Protocol State Machines nahtlos in eine IDL integrieren lassen; Dezyne und P zeigen, dass die vertragsbasierte Methodik heute aktueller denn je ist. Wer die erlaubten Ereignis-Reihenfolgen seiner Schnittstellen formal spezifiziert, findet Integrationsfehler früher und erhält zugleich eine präzise, automatisch auswertbare Dokumentation des Verhaltens. Die Wahl der konkreten Technologie ist dabei zweitrangig; entscheidend ist, dass der Vertrag mehr umfasst als Datentypen und Signaturen.

Custom Tools bei itemis — Wir entwickeln maßgeschneiderte Werkzeuge und Integrationen für Ihre Software-Entwicklungs-Toolchain: Custom Tools →