Andreas Vorwald hat sein Masterstudium an der TU Clausthal erfolgreich abgeschlossen. Das Thema seiner Masterarbeit lautet: „Formale Verifikation von Reaktiven Systemen am Beispiel einer Fahrzeugfunktion“.
Abstrakt:
„Der Nachweis der Korrektheit eines Systems gegenüber seine Systemspezifikation ist ein wichtiger Bestandteil im Entwicklungsprozess, vor allem für software-intensive Systeme die im sicherheitskritische Anwendungen eingesetzt werden. Um Korrektheit gegenüber der Systemspezifikation zu zeigen, kommen unterschiedliche Verifikationsmaßnahmen zum Einsatz. Üblicherweise werden komplexe Testfälle erstellt, die bestanden werden müssen. Jedoch können Testfälle die Korrektheit eines Systems nicht nachweisen. Aus diesen Grund gewinnt formale Verifikation in sicherheitskritischen Domänen an Bedeutung.
Um die Anwendbarkeit formaler Verifikationsverfahren zu zeigen, wird in dieser Arbeit ein Teil der Abgasnachbehandlung für Dieselmotoren der Volkswagen AG formal verifiziert. Das System liegt als ASCET-Systemmodell vor und berechnet eine Stellgröße für ein Ventil. Zunächst wurde eine informelle Systemanforderung in der formalen Anforderungsspezifikationssprache LTL spezifiziert. Mit Hilfe der formalen Systemanforderung wurde eine Komponente aus dem ASCET-Systemmodell ausgewählt, auf die sich die formale Systemanforderung direkt bezieht. Aus dieser Komponente wurde ein Datenfluss ausgewählt, welcher unter definierten Annahmen mathematisch beschrieben wurde. Dieser Datenfluss enthält eine lineare Interpolation, welche mit einer Kennlinie ein Zwischenergebnis berechnet.
Das mathematische Modell wurde mit Fehlermodellen versehen und durch den Model Checker KIND2 formal verifiziert. Es wurden zwölf Versuche mit vier Kennlinien durchgeführt. Durch die formale Verifikation wurde gezeigt dass Fehlermodelle in der Entwicklung eingebetteter Systeme beachtet werden müssen um die durch die Systemspezifikation angeforderte Ergebnisse erzielen zu können.“
