iSAQB CPSA-A FM

Beschreibung

Die Teilnahme am iSAQB® CPSA-A-Kurs „Formal Methods (FM)” bringt den Teilnehmenden 10 Credit Points in der Technischen Kompetenz (TC), 10 Credit Points in der Methodischen Kompetenz (MC) und 10 Credit Points in der Kommunikativen Kompetenz (CC) 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