iSAQB® CPSA-A - Formal Methods (Schulung)

Beschreibung

Die Teilnahme am iSAQB® CPSA-A-Kurs „Formal Methods (FM)” bringt den Teilnehmenden 20 Credit Points in der Technischen Kompetenz (TC) und 10 Credit Points in der Methodischen Kompetenz (MC) ein – anrechenbar auf die insgesamt 70 erforderlichen Credit Points für die Zulassung zur CPSA-A-Prüfung bei Brightest. Bitte beachten Sie, dass Sie im Rahmen der Zulassung zur CPSA-A-Prüfung bei Brightest in jedem der folgenden Kompetenzbereiche mindestens zehn Credit Points nachweisen müssen:

• Technische Kompetenz (TC)
• Methodische Kompetenz (MC)
• Kommunikative Kompetenz (CC)

Das akkreditierte iSAQB®-Training FM – Formal Methods (CPSA-A) basiert auf dem aktuellen iSAQB®-Lehrplan:

Teil 1 – Logik

• Grundstruktur der Aussagenlogik kennen
• Grundstruktur der Prädikaten- bzw. Prädikatenlogik erster Stufe kennen
• Grundstruktur temporaler Operatoren kennen
• Grundkonzepte eines logischen Kalküls verstehen
• Unterschied zwischen intuitionistischer und klassischer Logik verstehen

Teil 2 – Spezifikation und Implementierung

• Begriffe von Spezifikation unterscheiden können
• Verstehen, dass Spezifikationen sich auf unterschiedliche Arten von Komponenten beziehen können
• Verstehen, dass Spezifikationen sich auf unterschiedliche Qualitätsmerkmale beziehen können
• Unterschiede zwischen formalen und anderen Spezifikationstypen erkennen
• Eigenschaften von mindestens drei verschiedenen Spezifikationssprachen kennen
• Das Konzept der Verfeinerung verstehen

Teil 3 – Formale Methoden und der Entwicklungsprozess

• Erkennen, wo formale Methoden einsetzbar sind
• Relevante Qualitätsmerkmale für den Einsatz formaler Methoden kennen
• Die Bedeutung präziser Spezifikation verstehen
• Abwägungen zwischen verschiedenen formalen Methoden kennen
• Formale Methoden schrittweise einführen
• Geeignete formale Methoden auswählen
• Architekturen mit formalen Methoden bewerten

Teil 4 – Werkzeuge

• Property-based Testing anwenden
• Die Rolle von Typsystemen verstehen
• Model Checking anwenden, um Eigenschaften von Automaten zu überprüfen
• Proof Assistants einsetzen, um Eigenschaften beliebiger Softwaresysteme zu verifizieren
• SMT-Solver einsetzen, um Einschränkungen beliebiger Softwaresysteme zu verifizieren
• Abstrakte Interpretation anwenden, um dynamisches Verhalten statisch vorherzusagen