Dieser Lehrplan soll eine Sammlung formaler Methoden bereit­stellen, die das tradi­tio­nelle Arsenal von Architekt:innen ergänzen und ersetzen. Diese Methoden führen zu mathe­ma­ti­schen Beweisen kriti­scher System­ei­gen­schaften. Dabei ist zu beachten, dass solche Beweise in der Regel nicht nachträglich für die Archi­tektur eines Systems erbracht werden können. Statt­dessen muss die Archi­tektur von Anfang an so konzi­piert werden, dass sie für einen solchen Nachweis geeignet ist. Während das Entwerfen und Erstellen von Systemen, die für verschiedene Arten von automa­ti­sierten Tests geeignet sind – wie z. B. Unit‑, Integrations‑, Akzeptanz- und Eigen­schafts­tests – gängige Praxis ist und durch gängige Techno­logie-Stacks gut unter­stützt wird, ist der Aufwand für die Integration formaler Methoden in ein Design wesentlich höher. So erfordert beispiels­weise die Herstellung einer formalen Verbindung zwischen Spezi­fi­kation und Imple­men­tierung eine sorgfältige Auswahl der Spezi­fi­ka­tions- bzw. Programmiersprachen.

Um formale Methoden anwenden zu können, müssen Architekt:innen wichtige Eigen­schaften des Software­systems mathe­ma­tisch formu­lieren, eine Archi­tektur erstellen, die diese Eigen­schaften gewähr­leisten kann, und diese dann formal verifi­zieren. Die Erstellung einer Archi­tektur, die für die Verifi­zierung geeignet ist, erfordert sorgfältige Überle­gungen und ein hohes Maß an Architekturkompetenz.