Wie verbessern formale Methoden die Softwarearchitektur im Vergleich zu herkömmlichen Ansätzen und welche Herausforderungen bringen sie mit sich?

Dieser Lehrplan soll eine Sammlung formaler Methoden bereitstellen, die das traditionelle Arsenal von Architekt:innen ergänzen und ersetzen. Diese Methoden führen zu mathematischen Beweisen kritischer Systemeigenschaften. Dabei ist zu beachten, dass solche Beweise in der Regel nicht nachträglich für die Architektur eines Systems erbracht werden können. Stattdessen muss die Architektur von Anfang an so konzipiert werden, dass sie für einen solchen Nachweis geeignet ist. Während das Entwerfen und Erstellen von Systemen, die für verschiedene Arten von automatisierten Tests geeignet sind – wie z. B. Unit‑, Integrations‑, Akzeptanz- und Eigenschaftstests – gängige Praxis ist und durch gängige Technologie-Stacks gut unterstützt wird, ist der Aufwand für die Integration formaler Methoden in ein Design wesentlich höher. So erfordert beispielsweise die Herstellung einer formalen Verbindung zwischen Spezifikation und Implementierung eine sorgfältige Auswahl der Spezifikations- bzw. Programmiersprachen.

Um formale Methoden anwenden zu können, müssen Architekt:innen wichtige Eigenschaften des Softwaresystems mathematisch formulieren, eine Architektur erstellen, die diese Eigenschaften gewährleisten kann, und diese dann formal verifizieren. Die Erstellung einer Architektur, die für die Verifizierung geeignet ist, erfordert sorgfältige Überlegungen und ein hohes Maß an Architekturkompetenz.