Verifikation von Software

Für sicherheitskritische Systeme ist es erforderlich, die Korrektheit der Software objektiv nachzuweisen. Dafür wird der Einsatz formaler Methoden von den einschlägigen Normen dringend empfohlen. Beispiele sind Signalisierungsanlagen in der Bahntechnik, Steuercomputer in Flugzeugen oder Regelungen medizinischer Geräte. In den letzten Jahren sind formale Verifikations- und Analysemethoden so weit entwickelt worden, dass sie auch für industriell relevante Probleme einsetzbar geworden sind. Bei der Modellprüfung (Model Checking) wird ein Modell des Systems bezüglich einer temporallogischen Eigenschaft überprüft, und bei der dynamischen Analyse werden Laufzeiteigenschaften bezüglich spezifizierter Anforderungen untersucht. Zu den Eigenschaften, die formal nachweisbar sind, gehören z.B. die Abwesenheit von arithmetischen Überläufen bzw. Nulldivisionen oder die Erreichbarkeit von Fehlerzuständen und Lokalisierung „toten“ Codes.

Das Modul behandelt Methoden zur deduktiven Verifikation, bei der die Beweise interaktiv vom Benutzer mit einem Beweissystem geführt werden, sowie automatische Verifikationsverfahren, die in der industriellen Praxis eingesetzt werden. Die Vorlesung gibt einen Überblick über die wichtigsten formalen Methoden zur Software-Verifikation. In den Übungen erlernen die Teilnehmer, wie die entsprechenden Methoden in der Praxis eingesetzt werden können. Es wird das praktische Arbeiten und der Umgang mit verbreiteten Werkzeugen der Verifikation von Software geübt