Formale Methoden für konkurrierende Systeme

Gleichzeitigkeit ist das A und O der heutigen Softwarearchitektur. Selbst einfache Systeme müssen mit Datenbanken oder Webservices kommunizieren, was neue Herausforderungen in Bezug auf Zuverlässigkeit und Datenkonsistenz mit sich bringt. Wenn Microservices und Caches ins Spiel kommen, wird die Landschaft noch schwieriger. In solchen Situationen ist es sehr nützlich, über unser System auf einer höheren Ebene nachzudenken und sich auf die wichtigsten Funktionen zu konzentrieren und nicht auf die winzigen Details wie die spezielle Bibliothek, die Sie für die Serialisierung verwenden. Formale Methoden sind ein wirklich wertvolles Werkzeug auf dieser Reise.

Formale Methoden ist ein Überbegriff für alle Techniken, die während des Entwicklungszyklus angewendet werden und auf Logik, theoretischer Informatik oder Mathematik basieren. Das Typsystem in einer statisch typisierten Programmiersprache ist ein gutes Beispiel: In diesem Fall ist die zugrundeliegende logische Grundlage die Typentheorie. Die meisten Formen der Analyse, wie z.B. die Nullbarkeit in Kotlin, geprüfte Ausnahmen in Java und der Borrow Checker von Rust, sind ebenfalls von der Logik geprägt.

Da formale Methoden ein so unscharfes Konzept sind, ist es üblich, sie je nach der Phase, in der sie angewendet werden, mit unterschiedlichen Namen zu bezeichnen. Das folgende Diagramm zeigt drei große Kategorien, die aber wie üblich alle miteinander verbunden sind. Der Versuch, einen Teil des Codes formal zu überprüfen, kann uns beispielsweise dabei helfen, unser Modell zu verfeinern, das wiederum zusätzliche Informationen für eine bestimmte statische Analyse liefern kann.

Formale Methoden unterstützen eine breite Palette von Technologien und Produkten, nicht nur nebenläufige Systeme. Hardware-Design und -Verifizierung ist ein weiterer Bereich, in dem diese Techniken eine größere Rolle spielen. In unserem Fall nutzen wir unsere Erfahrung beim Entwurf verteilter Architekturen, um die Qualität der in diesen Bereichen entwickelten Produkte zu verbessern.

Modellierung

Eine der schwierigsten Aufgaben in einem nebenläufigen System ist die Sicherstellung der Datenkonsistenz und -integrität über eine Abfolge von Schritten, von denen jeder möglicherweise von einem anderen Akteur ausgeführt wird. Um konkreter zu werden, lassen Sie uns das unten abgebildete System betrachten, das einen sehr einfachen Webshop beschreibt. Jedes Rechteck entspricht einem Zustand, in dem sich der Vorgang befinden kann: Der Kunde kauft ein, indem er Artikel hinzufügt, und irgendwann checkt er aus und bezahlt dann.

Indem wir das System in dieser Form visualisieren, beseitigen wir bereits eine Menge zufälliger Komplexität (für unsere Zwecke), z.B. woher wir wissen, welche Artikel verfügbar sind und bei jedem Schritt ausgewählt wurden (vielleicht eine mobile App, vielleicht eine Website). Aber selbst mit einem so einfachen Modell können wir potenzielle Probleme untersuchen, wie z.B. doppelte Checkouts oder korrekte Zahlungen, die nicht zu einer Lieferung führen. Jede Prüfung, die unserem Modell hinzugefügt werden musste, wird in der einen oder anderen Form in der tatsächlichen Implementierung repliziert.

Wir wiederholen unser Modell so lange, bis wir von seiner Korrektheit überzeugt sind. Dabei sind Modellprüfprogramme wie TLA+ und Alloy eine wichtige Hilfe. Anhand einer Beschreibung wie dem obigen Diagramm können Sie dem Model Checker Fragen stellen, z.B.: "Gibt es eine Abfolge von Aktionen, die dazu führt, dass ich mehr Artikel verkaufe als im Laden verfügbar sind?" Wenn die Antwort "Ja" lautet, wird ein Beispiel für eine solche Abfolge angegeben. Dies hat erhebliche praktische Auswirkungen: Auf der TLA+ Website finden wir zwei Beispiele für Fehler in ElasticSearch und Kafka - zwei wichtigen Komponenten in verteilten Architekturen - die aufgrund des Modells gefunden wurden, noch bevor ein Benutzer ein fehlerhaftes Verhalten gemeldet hat. Ein weiterer Beleg für die Leistungsfähigkeit dieser Tools ist, dass sowohl Amazon als auch Microsoft sie eingesetzt haben, um das Vertrauen in einige der Algorithmen zu erhöhen, die ihren Cloud-Angeboten zugrunde liegen.

Statische Analysen

Bei der formalen Modellierung geht es vor allem darum, das System auf einer tieferen Ebene zu verstehen, in der Regel während der Entwurfsphase; das Gegenstück für die Implementierungsphase sind statische Analysen. Mit ihnen können wir potenzielle Probleme beim Schreiben oder Kompilieren des Codes aufspüren, bevor er in irgendeiner Form ausgeführt wird. Wie bereits erwähnt, sind Typsysteme ein bekanntes Beispiel, die in der Regel in Editoren und IDEs integriert sind.

In der Abteilung für funktionale Programmierung bei Xebia sind wir glückliche Nutzer leistungsfähiger Typsysteme wie das von Scala, die es uns ermöglichen, die Überprüfung vieler Dateninvarianten an den Compiler auszulagern. Und nicht nur das: Ein Typsystem hilft uns, indem es mit automatischer Ableitung und anderen Techniken Kauderwelsch entfernt. Verfeinerung und abhängige Typen sind der nächste Schritt auf der Leiter, der es dem Entwickler ermöglicht, die Eigenschaften jedes einzelnen Datenteils sowie die Beziehungen zwischen ihnen zu beschreiben.

Leider klafft eine große Lücke zwischen dem, was die Forschung bietet, und dem, was der "gewöhnliche Entwickler" bei seiner täglichen Arbeit zur Verfügung hat. Ein wichtiger Grund für diese Kluft ist der Mangel an Tools, die oft unausgereift sind oder sich an Experten richten. Projekte wie Arrow Analysis überbrücken diese Lücke, indem sie nützliche und bewährte Ideen in Sprachen wie Kotlin einbringen.

Formale Methoden @ Xebia

Auch wenn es andere Unternehmen im Bereich der formalen Methoden gibt, ist es unser Ziel, diese Methoden dem "normalen Entwickler" näher zu bringen und sie nicht nur einigen wenigen Experten vorzubehalten. Wenn Ihr Team diese zusätzliche Ebene des Verständnisses und des Vertrauens in Ihre Software erreichen möchte, sind wir bereit, Ihnen mit formalen Methoden zu helfen. Umgekehrt, wenn Sie Unternehmen dabei helfen möchten, ihr formales Spiel zu verbessern, haben wir offene Stellen für Ingenieure für formale Methoden.