Über das neue CPSA® – Advanced Level Modul FM: Formale Methoden

Am 27. Februar 2025 führte das iSAQB das neue Advanced Level-Modul Formale Methoden (FM) ein.

Das Modul „FM – Formale Methoden“ vermittelt Software­ar­chi­tekten, wie sie die Korrektheit des Designs und der Imple­men­tierung eines Systems durch mathe­ma­tische Beweise sicher­stellen können. Das Modul konzen­triert sich auf sicher­heits­kri­tische, sensible oder wirtschaftlich vitale Systeme und geht über tradi­tio­nelle Archi­tektur- und Testme­thoden hinaus, indem es formale Techniken bietet, um zu überprüfen, dass Software ihren Anfor­de­rungen entspricht. Durch die frühzeitige Integration formaler Methoden in der Design­phase können Archi­tekten verifi­zierbare Modelle erstellen, die ein höheres Maß an Software­qua­lität und Zuver­läs­sigkeit gewährleisten.

Wir haben ein Interview mit den Kuratoren, Michael Sperber und Lars Hupel, geführt, in dem sie tiefere Einblicke in das Modul geben.

Warum ist das Thema „Formale Methoden“ aus eurer Sicht so wichtig, dass es ein eigenes Modul im CPSA Advanced-Programm verdient?

Software­systeme steuern immer mehr Aspekte unseres Lebens, und damit wird zunehmend die Sicherheit dieser Systeme relevant, und zwar im doppelten Sinne: Die Sicherheit, wenn es um Leib, Leben oder
unter­neh­mens­kri­tische Bereiche geht, und die Sicherheit vor Einbrüchen, Sabotage und Datenen­lecks. Bei solcher Software wollen wir, dass die Software bestimmte Anfor­de­rungen garan­tiert erfüllt. Dafür reichen einfache Tests nicht aus, die ja in der Regel nur bestimmte Szenarien abdecken – wir wollen, dass die Software sich in allen Szenarien korrekt verhält. Es braucht die Anwendung mathe­ma­ti­scher Techniken – sogenannter formaler Methoden, und die waren bisher eine Lücke im Portfolio der Advanced-Schulungen, die wir jetzt geschlossen haben.

Welche konkreten Vorteile bieten formale Methoden im Vergleich zu tradi­tio­nellen Software­ent­wick­lungs­an­sätzen, besonders in sicher­heits­kri­ti­schen Bereichen?

Sie leisten etwas, was tradi­tio­nelle Ansätze eben nicht leisten: Sie geben uns Garantien, statt einem bloßen Versprechen, dass ein Sicher­heits­problem mit dem nächsten Update behoben wird.

Wie unter­stützt das Modul Software­ar­chi­tekten dabei, die System­ge­nau­igkeit und ‑korrektheit in komplexen Projekten zu gewährleisten?

Der erste wichtige Aspekt ist, die Teile eines Systems zu identi­fi­zieren, bei denen die Anwendung bei formaler Methoden sich lohnt. Der zweite ist, abhängig von den Anfor­de­rungen die richtige formale Methode auszu­wählen: Inzwi­schen gibt es ja einen bunten Strauß davon. Schließlich geht es außerdem darum, in einem Projekt die techni­schen Voraus­set­zungen zu schaffen, dass formale Methoden effektiv zum Einsatz kommen können.

Formale Methoden sind bekannt für ihren mathe­ma­ti­schen Ansatz – wie lässt sich dieser in die Praxis umsetzen, ohne die Agilität der Entwicklung zu beeinträchtigen?

Prinzi­piell sind formale Methoden kein Wider­spruch zur Agilität. Aller­dings muss man ein ein paar grund­le­gende Überle­gungen zum Anfang des Projekt treffen. Das liegt daran, dass es aufwendig ist, formale Methoden nachträglich anzuwenden. Will ich zum Beispiel die Korrektheit eines bestimmten Stücks Codes beweisen, dann muss der in der Regel auf eine bestimmte Art und Weise geschrieben sein, und auch die Program­mier­sprache spielt eine Rolle. Viel effek­tiver ist es, die formalen Methoden begleitend zum Entwick­lungs­prozess zu benutzen und das Tooling dafür in die CI einzu­bauen. Damit ist es auch agil.

Welchen Einfluss haben formale Methoden auf die langfristige Wartbarkeit und Erwei­ter­barkeit von Softwarearchitekturen?

Der promi­nente Infor­ma­tiker Conal Elliott hat den Satz geprägt „Only correctness composes“: Wenn ein Softwarebau­stein eine Eigen­schaft sicher erfüllt, dann ist es vollkommen egal, wie das passiert, und ich kann es mit anderen solchen Bausteinen sicher kombi­nieren, ohne dass ich mir Sorgen um die innereren Details machen muss. Das fördert die Entkopplung der Bausteine und ist damit großartig für die Architektur.

Welche Voraus­set­zungen sollte man für dieses Modul mitbringen, insbe­sondere im Hinblick auf mathe­ma­tische Kennt­nisse und Vorkennt­nisse in Softwarearchitektur?

Gymna­si­al­ma­the­matik genügt. Die Schulung ist prinzi­piell unabhängig von den anderen Advanced-Schulungen, passt aber besonders gut zu FUNAR und EMBEDDED: Zu FUNAR, weil formale Methoden in der Praxis eh auf funktio­naler Program­mierung aufbauen und EMBEDDED, weil es im Embedded-Bereich häufig erhöhte Anfor­de­rungen an Quali­täten gibt, bei denen formale Methoden helfen können.