Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage:

- Gängige Methoden für das Testen von Software anzuwenden (wie Aquivalenzklassen, Boundary Testing, Abdeckungsmetriken

- Assertions in der Softwareentwicklung einzusetzen um die Qualität der Software zu erhöhen

- Software mit Vor- und Nachbedingungen zu spezifizieren und Korrektheit mit Invarianten und Hoare Logik zu beweisen

- Automatische Softwareverifikationstools wie Bounded Model Checking und Symbolische Simulation einzusetzen

• Methoden der Modellierung und Spezifikation durch Logik, Automaten, Assertions, Coverage Kriterien
• Verifikationswerkzeuge, insbesonders Model Checker, Statische Analyse, Theorembeweisen, Testen
• Praktischer Umgang mit Verifikationswerkzeugen
• Grundlagen zur Zertifizierung und zu Standards in der industriellen Validierung

- Lösen von Übungsaufgaben

- Einsatz von Softwareverifikationstools zum Auffinden von Softwarefehlern

ECTS Breakdown:

36h Vorlesung
114h Übungen
---------------------------
150h in Summe (6 ECTS)
---------------------------

Die Studenten lösen Übungsaufgaben (von Hand oder mit Softwarewerkzeugen) und reichen diese ein. Die Abgaben werden kommentiert und bewertet.