Wir haben formale Architekturverifikation als überraschend günstiges, effektives und breit einsetzbares Werkzeug der Qualitätssicherung entdeckt. TLA+ ist eine der verbreiteten Technologien in dem Kontext. Man sollte sich nicht von der etwas alt anmutenden Projektwebseite abschrecken lassen. Amazon hat zum Beispiel TLA+ für DynamoDB eingesetzt und andere große Firmen nutzen es, seitdem wie davor, auch immer wieder. Wir glauben, dass formale Architekturverifikation ein unterschätztes Werkzeug ist, das mehr Aufmerksamkeit verdient. In diesem Artikel möchten wir darüber sprechen, wo der Einsatz formaler Architekturverifikation Sinn ergeben würde. Etwas vorausgreifend sei angedeutet, dass wir viele Anwendungsfälle im Gesundheitssektor sehen, seien es z.B. KIS (Krankenhausinformationssysteme), LIS (Laborinformationssysteme), Patientenakten (z.B. die ePA für alle oder andere proprietäre Akten) oder nicht zuletzt medizinische Geräte wie z.B. Herzschrittmacher, Insulinpumpen oder Apps, die diese verwalten.
Hinweis: Es gibt auch eine Englische Version dieses Artikels.
Ein kleiner Absatz noch dazu, was formale Architekturverifikation überhaupt ist: Wenn man eine Architektur erstellt, designt man bereits die Interaktion der unterschiedlichen Architekturkomponenten. Wenn man nun wissen möchte, ob die algorithmischen Bedingungen (d.h. z.B. Zeitbedingungen aber nicht Interfacekompatibilität) korrekt sind, kann formale Architekturverifikation helfen. In UML Begriffen kann diese Methode hauptsächlich auf Zustandsdiagramme, Flussdiagramme oder Sequenzdiagramme angewendet werden. Man wird nun die Architektur in der Sprache des Verifikationswerkzeuges modellieren. Danach wird werkzeuggestützt, ein formaler mathematischer Beweis für die zu prüfenden Bedingungen erstellt. Bei TLA+ wird man in der Regel auf die relevanten Probleme hingewiesen, falls kein Beweis gefunden werden konnte. Auf diesem Wege hilft formale Architekturverifikation dabei, sowohl größere Probleme als auch subtilere Unzulänglichkeiten zu finden und zu beheben, bevor überhaupt die erste Zeile Produktionscode geschrieben wurde.
Bevor wir gleich zu den Einsatzbereichen formaler Architekturverifikation kommen, müssen wir allerdings eine wichtige Frage beantworten:
Gibt es einen Unterschied zwischen formaler Verifikation und formaler Architekturverifikation?
Kurz zusammengefasst: Ja: Sowohl in den Kosten als auch in der Stärke des Ergebnisses gibt es Unterschiede.
Etwas länger ausgeführt: Wenn Leute von formaler Verifikation sprechen, meinen sie in der Regel formale Quelltextverifikation, also einen mathematischen Beweis für die Korrektheit des tatsächlich eingesetzten Quelltextes erbringen. Formale Quelltextverifikation trifft eine wesentlich stärkere Aussage über das Gesamtsystem und lässt weniger Raum für Bugs. Allerdings ist es auch wesentlich aufwändiger und komplexer und beeinflusst die Technologieauswahl.
Wir mögen formale Architekturverifikation, weil sie kosteneffizient ist und angewendet werden kann, noch bevor die erste Zeile Code geschrieben wurde. Dadurch sind wesentlich effizientere, kurze Arbeitszyklen möglich.
Ok, wann sollte ich formale Architekturverifikation verwenden?
Wir glauben zunächst einmal, dass jeder gute Anwendungsfall für formale Quelltextverifikation auch ein guter Anwendungsfall für formale Architekturverifikation ist. Aufgrund der geringeren Kosten sehen wir aber wesentlich mehr, sinnvolle Anwendungsfälle für formale Architekturverifikation. Im Folgenden führen wir eine informelle Liste überlappender Kategorien von Anwendungsfällen auf, bei denen wir glauben, dass formale Architekturverifikation sinnvoll eingesetzt werden kann.
Risiko für öffentliche Grundversorgung inkl. öffentlicher Sicherheit
Jemals den Wasserhahn angeschaltet und unsauberes oder gar kein Wasser vorgefunden? Das möchte sicherlich niemand. Wasserwerke und -netze mit der sie steuernden Software sind lebenswichtig und formale Architekturverifikation kann hier einen Mehrwert bieten. Ähnliche Fälle sind Elektrizitätsversorgung, Netzwerke und Router sowie Notrufhotlines inklusive der damit verbundenen Leitstellensysteme.
Risiko für Integrität kritischer Daten
Wahlen sind äußerst wichtig für Demokratien. Manche Länder verwenden Wahlcomputer zur Erfassung von Stimmen, andere Ländern nutzen Software lediglich für die weitere Verarbeitung der ausgezählten Stimmen. Die Korrektheit und Sicherheit dieser Systeme ist essenziell für das Vertrauen in die Wahl. Hier ist ein Beispiel falscher Sitzverteilung bei sächsischen Wahlen, die vermutlich durch den Einsatz formaler Architekturverifikation vielleicht vermeidbar gewesen wäre. Da ausgezählte Stimmendaten oft über mehrere hierarchische Schichten gereicht werden, wäre sicherlich auch eine formale Verifikation der Gesamtarchitektur sinnvoll.
Es gibt auch andere kritische Daten, die integer bleiben müssen – zum Beispiel bei Systemen zur Verwaltung von Asylanträgen oder Sozialleistungen, Blutkonserven, Transplantationslisten oder bei der Verarbeitung von Daten, die Leute von der modernen Lebensführung ausschließen können. Bei letzterem denken wir an Flugverbotslisten (hier insb. die Begründung) oder Kontensperrungen bei Gatekeepern, wie Google (Wir wünschen z.B. viel Freude dabei, ohne Konto bei Google oder Apple ein Busticket in Straßburg zu kaufen).
Risiko für große finanzielle Verluste
Sobald die eigene Existenz im finanziellen Risiko steht, ist es vermutlich Wert, einige Tage Aufwand in formale Architekturverifikation zu investieren. Das ist einfaches Risikomanagement. Unter der Annahme, dass in einfachen Fällen formale Architekturverifikation mit weniger als einer Personenwoche Aufwand umsetzbar ist, wird es eine gute risikomindernde Maßnahme für Risiken ab 100k€ mit erhöhter Eintrittswahrscheinlichkeit (1 mal alle 3 Jahre) oder vielleicht auch für Risiken ab 50k€ mit hoher Eintrittwahrscheinlichkeit (1 mal pro Jahr). Das sind natürlich nur Beispielwerte, die im konkreten Fall im Risikomanagement genauer betrachtet werden müssten.
Von dieser abstrakten Perspektive kommend, widmen wir uns nun praktischeren Beispielen. Wir haben zwei solche Beispiele, die aus unserer Sicht recht klar sind: automatische (Börsen-)Tradingsysteme und Smart Contracts, weil diese z.T. sehr schnell sehr viel Geld vernichten können. Das andere Beispiel ist die Raumfahrt. Dort steht in der Regel sehr viel Geld auf dem Spiel und in manchen Fällen gibt es kaum oder gar keine Alternativen, Probleme nach dem Raketenstart zu beheben. Die Systeme sind, insbesondere in der Forschung, in der Regel einzigartig und praktisch unersetzbar.
Risiko für Leib und Leben
Ob es nun ein Herzschrittmacher, eine Insulinpumpen-App, eine Bestrahlungsmaschine, ein control-by-wire System eines Fahrzeugs, der Türabschalter einer CNC-Fräse oder ein Feueralarmsystem ist; formale Architekturverifikation sollte hier wirklich durchgeführt werden. Natürlich sollte es nicht die einzige Qualitätssicherungsmaßnahme sein. Eine unvollständige Liste weiterer Beispiele, die uns einfallen, wäre: Elektronische Verschreibungssysteme (eRezept), Patientenakten, Operationsticketsysteme oder auch Präsenzsysteme in Bergwerken, auf deren Basis die Freigabe zur Sprengung gegeben wird.
Risiko für große Katastrophen
Wer kann sich noch daran erinnern, dass Amsterdam 2023 beinahe überflutet wurde? Dieses System, wie auch andere Wehr- und Schleusensteuerungssysteme, wären gute Kandidaten für formale Architekturverifikation. Und es würde nicht schaden, die manuellen Bedienschritte und den Fahrtweg zur Schleuse in die Architektur mit einzubeziehen. Wir glauben, dass dieser Vorfall damit vermieden worden wäre.
Andere solche Katastrophen bzw. katastrophenrelevante Systeme könnten sein: Kernschmelzen von Kernreaktoren, Notstromversorgung auf (Kreuzfahrt-) Schiffen, Katastrophenwarnsysteme oder konkreter Erdbebenwarnsysteme.
Zusammengefasst
Wir meinen, dass die Anwendung formaler Architekturverifikation als Qualitätssicherungsmaßnahme insbesondere, aber nicht ausschließlich, im Gesundheitsbereich sinnvoll ist und ggf. sogar die Norm werden sollte. Wer jetzt technische Details sehen möchte, darf gespannt auf einen weiteren Blogpost von uns warten, der mehr auf die technischen Details und die praktische Anwendung eingeht.
Kommentar verfassen