iSAQB® FM - Formale Methoden

Es gibt Systeme, bei denen ein übersehener Fehler Hardware zerstört, sensible Daten preisgibt oder Beträge falsch berechnet. Für diese Systeme bündelt das iSAQB Modul FM die Verfahren, die mathematisch klären, ob eine Eigenschaft gilt. Du arbeitest an Logik, an Spezifikationssprachen wie Isabelle/HOL, TLA+ und Alloy und an der Frage, wo sich der Aufwand lohnt. Der iSAQB verlangt ein durchgearbeitetes Beispiel, du siehst die Verfahren also einmal vollständig angewendet.

iSAQB® Akkreditierter TrainingspartnerTeilnahmezertifikat4,8/5 bei ProvenExpert

Was dieses Modul leistet.

Wo ein Architekturreview ein Urteil abgibt, liefert FM einen maschinell geprüften Beweis. Im tecnovy Training spezifizierst du kritische Eigenschaften formal und weist sie mit Model Checkern, Beweisassistenten und SMT-Solvern nach. Korrektheit wird belegbar statt behauptet.

So läuft das Training

Methode: Beweise am Werkzeug führen, ein Praxisbeispiel durchrechnen
Grundlage: Offizieller iSAQB Lehrplan FM 2024.1-rev2, englischsprachig
Abschluss: 30 Credit Points: 10 methodisch, 20 technisch, keine Prüfung im Kurs

Termine & Buchung

Passenden Termin wählen

2 Termine

Termine mit diesem Symbol bieten bis zu 25 % Gruppenrabatt. Klicke auf „Details“, um mehr zu erfahren.

Okt 2026 1 Termin

05.–07. Okt 2026MESZ

Mo–Mi 09:00–17:00

Deutschland Gruppenrabatt

Stadt Hamburg

Sprache Deutsch

Trainer MS Dr. Michael Sperber

Plätze 5+ frei

10% Earlybird Rabatt

~~2.669 $~~−267 $2.402 $

zzgl. MwSt.

Nov – Dez 2026 1 Termin

30.–02. Nov – Dez 2026MEZ

Mo–Mi 09:00–17:00

Online-Training Gruppenrabatt

Zeitzone MEZ

Sprache Deutsch

Trainer MS Dr. Michael Sperber

Plätze 5+ frei

10% Earlybird Rabatt

~~2.311 $~~−232 $2.079 $

zzgl. MwSt.

Passung

Für wen das Modul gedacht ist

Typische Rollen

Du verantwortest Systemteile, deren Fehlverhalten Menschen, Geld oder Daten gefährdet.
Du musst Korrektheit belegen, wo Testabdeckung als Nachweis nicht ausreicht.
Du entscheidest, welche Prüfverfahren in die Werkzeugkette eines Projekts kommen.

Voraussetzungen

Keine Voraussetzungen

Du kannst direkt einsteigen. Mitbringen: Grundkenntnisse in Algebra und Logik. Hilfreich: Erfahrung mit funktionaler Programmierung, Vertrautheit mit der Semantik von Programmiersprachen.

Stattdessen geeignet FUNAR Steckt 600 von 1080 Minuten in funktionale Modellierung und Makroarchitektur und kommt ohne Beweisassistenten und Model Checker aus.

Lehrplan

CPSA® FM Kurs im Detail

Der Lehrplan 2024.1-rev2 gliedert FM in fünf Teile mit 1080 Unterrichtsminuten, von denen 415 auf Übungen entfallen. Er beginnt bei der Logik, führt über Spezifikationssprachen und die Einordnung im Entwicklungsprozess zu den Werkzeugen und endet bei einem durchgerechneten Beispiel. Eine offizielle deutsche Fassung gibt es nicht; die Titel hier sind unsere Übersetzung.

01Logik

Dieser Teil legt die Sprache fest, in der später jede Zusage formuliert wird.

Aussagenlogik: Syntax, Semantik, Normalformen, Entscheidbarkeit
Prädikatenlogik erster Stufe mit Quantoren, Skolemisierung und Substitution
Temporale Operatoren und der Unterschied zwischen LTL und CTL
Kalküle: natürliches Schließen, Sequenzenkalkül, Resolution

02Spezifikation und Implementierung

Hier entsteht die Spezifikation, gegen die anschließend bewiesen wird.

Beispiele, Eigenschaften, formale und mechanisierte Spezifikation unterschieden
Spezifikationen für Funktionen, Datentypen, Algorithmen und ganze Systeme
Qualitäten wie Funktionalität, Performance, Security und Safety spezifizieren
Isabelle/HOL, ACL2, TLA+ und Alloy sowie der Begriff des Refinements

03Formale Methoden und der Entwicklungsprozess

Der kürzeste Teil beantwortet die teuerste Frage: wo sich der Aufwand lohnt.

Das SPE-Modell als Raster für die Genauigkeit einer Spezifikation
Abwägung zwischen Ausdrucksstärke, Aufwand und nötiger Qualifikation
Schrittweiser Einstieg über statische Typisierung und Property-based Testing
Architekturbewertung mit SMT/SAT-Solving und abstrakter Interpretation

04Werkzeuge

Hälftig Übung: 150 der 300 Minuten stehen für die Arbeit am Werkzeug.

Property-based Testing und was Typsysteme bis hin zu abhängigen Typen zusichern
Model Checking über endliche Automaten, BDD, CTL und PLTL
Beweisassistenten und SMT-Solver für beliebige Softwaresysteme
Abstrakte Interpretation als statische Vorhersage dynamischen Verhaltens

05Beispiele

Zum Abschluss wird ein vollständiges Beispiel durchgerechnet, statt weiter über Verfahren zu reden.

Mindestens ein durchgerechnetes Beispiel ist in jeder lizenzierten Schulung Pflicht
180 Minuten, davon 60 als Übungszeit
Art und Aufbau der Beispiele gibt der iSAQB bewusst nicht vor
Sie dürfen den Systemen und Interessen der Teilnehmenden folgen

Offizieller Lehrplan

Ergebnis

Was du anschließend leisten kannst

01
Du formulierst kritische Systemeigenschaften in Aussagen- und Prädikatenlogik statt in Prosa.
02
Du vergleichst Isabelle/HOL, ACL2, TLA+ und Alloy nach Ausdrucksstärke und Aufwand.
03
Du bestimmst mit dem SPE-Modell, welche Systemteile sich formal prüfen lassen.
04
Du zerlegst ein System so, dass sich Komponenteneigenschaften zu Systemeigenschaften zusammensetzen.
05
Du führst formale Methoden schrittweise über statische Typisierung und Property-based Testing ein.
06
Du weist Eigenschaften endlicher Automaten per Model Checking nach.
07
Du übersetzt Projektanforderungen in Beweisverpflichtungen für einen Beweisassistenten.
08
Du prüfst Constraints eines Softwaresystems mit SMT-Solvern.

Credit Points für CPSA-A

Methodische Kompetenz: 10
Technische Kompetenz: 20
Kommunikative Kompetenz: 0

30 von 70 Punkten für die CPSA-A Zulassung

Credit Planner öffnen iSAQB Board → Regeln zu Credit Points Leitfaden →

Teilnahmezertifikat

Das tecnovy Teilnahmezertifikat weist deine Teilnahme am FM Training aus, keine bestandene Prüfung.

Certificate Showroom öffnen tecnovy →

≥80%Anwesenheit

Trainer:innen

Dr. Michael Sperber

iSAQB®

Warum tecnovy

Was du bei uns oben drauf bekommst

iSAQB® Akkreditierter Anbieter

Wir sind ein offiziell akkreditierter Schulungsanbieter des International Software Architecture Qualification Board.

Certificate Showroom

Hol dir dein Teilnahmezertifikat und verbinde es, falls vorhanden, mit deinem Prüfungszertifikat. Vollautomatisiert, schön gestaltet. Nur für dich, nur bei tecnovy.

No Slideshow, Hands-On!

Versprochen: keine PowerPoint-Schlacht. Wir arbeiten in Gruppen, verknüpfen Theorie mit Praxis, und du bekommst Praxisbeispiele unserer erfahrenen Trainer sowie den Austausch mit Gleichgesinnten.

Doppelt hält besser

Gerne darfst du innerhalb eines Jahres die Schulung nochmals online als Refresher besuchen.

Lerne von Experten

Wir garantieren dir stets den Einsatz von didaktisch und methodisch erstklassig qualifizierten Trainern, die ihr Wissen sowohl aus Trainingserfahrung als auch beruflicher Praxis- und Projekterfahrung beziehen.

Flexible Umbuchung

Falls du mal kurzfristig verhindert sein solltest, kannst du deine Schulung bis eine Woche vor Trainingsbeginn kostenlos umbuchen.

FAQs

Häufige Fragen

01Brauche ich CPSA-F, um am FM Training teilzunehmen?

Nein. Der iSAQB Lehrplan zum Modul FM nennt als Voraussetzungen Grundkenntnisse in Algebra und Logik, keine Zertifizierung. Für die spätere CPSA-A Zertifizierung ist CPSA-F dagegen Pflicht.

02Gibt es eine FM Prüfung?

Nein. Für das Modul FM existiert keine eigene Prüfung. Das tecnovy FM Training bringt dir 30 Credit Points und ein Teilnahmezertifikat; geprüft wird erst modulübergreifend auf dem Weg zur CPSA-A Zertifizierung.

03Wie viele Credit Points bringt FM?

FM bringt dir im tecnovy Training 30 Credit Points, aufgeteilt in 20 technische und 10 methodische. Der kommunikative Bereich bleibt bei null, was du einplanen solltest: die CPSA-A Zulassung verlangt 70 Punkte insgesamt und mindestens 10 in jedem der drei Kompetenzbereiche. Der iSAQB kann die Punktevergabe alle 12 Monate neu bewerten; die Angaben hier haben den Stand August 2026.

04Wie läuft die CPSA-A Zertifizierung ab?

Die CPSA-A Zertifizierung besteht aus einer Hausarbeit. Zwei vom iSAQB anerkannte Prüfer:innen bewerten sie, danach verteidigst du sie im Gespräch. Ablegen kannst du auf Deutsch oder Englisch, und bei Fragen zum Ablauf hilft dir tecnovy gerne weiter.

05Wie lange dauert das FM Training?

Das tecnovy FM Training dauert drei Tage. Der iSAQB Lehrplan setzt als Minimum drei Tage und 1080 Unterrichtsminuten an, also 18 Zeitstunden, verteilt auf fünf Teile. 415 dieser Minuten sind als Übungszeit ausgewiesen.

06Was unterscheidet FM von FUNAR?

FM weist Eigenschaften eines Systems mit Logik, Beweisassistenten, Model Checkern und SMT-Solvern nach. FUNAR entwirft Systeme funktional und steckt 600 seiner 1080 Minuten in funktionale Modellierung und Makroarchitektur, ohne Beweiswerkzeuge. Beide Module bringen dieselben 30 Credit Points im Verhältnis 20 technisch zu 10 methodisch, die Punkte entscheiden für dich also nichts.

07Wie viel Mathematik brauche ich für FM?

Grundkenntnisse in Algebra und Logik solltest du mitbringen, mehr verlangt der iSAQB Lehrplan zum Modul FM nicht. Die 180 Minuten des ersten Teils bauen die Logik gemeinsam auf, von der Aussagenlogik über die Prädikatenlogik bis zu temporalen Operatoren. Ein Mathematikstudium ist keine Voraussetzung für das tecnovy FM Training.

08Ist FM ein rein theoretisches Modul?

Nein, der Lehrplan reserviert einen eigenen fünften Teil für durchgerechnete Beispiele und verpflichtet jede lizenzierte Schulung, mindestens eines davon vorzuführen. Insgesamt sind 415 der 1080 Minuten als Übungszeit ausgewiesen, allein 150 davon im Teil Werkzeuge. Dieser fünfte Teil ist zugleich der einzige, den der Lehrplan ausdrücklich nicht als prüfungsrelevant führt.

09Bekomme ich die Flipcharts aus dem FM Training?

Ja. Alle Flipcharts, die während der drei Tage des tecnovy FM Trainings entstehen, bekommst du danach als Fotoprotokoll.

Wie sieht deine Schulung bei tecnovy aus?

FMFM - Formale Methoden

Bereit für den nächsten Schritt?

Wähle einen öffentlichen Termin oder plane das Training für dein Team.