Förderprojekte

Förderbeginn 01.07.2008

Runtime Verification - Von der Raumfahrt zum Automobil

PD Dr. Martin Leucker
Technische Universität München
Lehrstuhl für Informatik IV - Software & Systems Engineering

Dr. Klaus Havelund
NASA Jet Propulsion Laboratory
Laboratory for Reliable Software

Runtime-Verification ist eine einfache aber effektive Verifikationstechnik, die einerseits traditionelle Techniken wie Model-Checking und Testen abrundet, andererseits aber auch die Möglichkeiten der Verifikation erweitert. Da die Verifikation zur Laufzeit stattfindet, kann bei der Erkennung eines Fehlers auf diesen reagiert werden und dieser ggf. behoben werden. Im Rahmen diese Projektes wird der State-Of-The-Art von Runtime-Verification und die praktische Anwendbarkeit weiterentwickelt. Insbesondere werden die primär für den Weltraumbereich entwickelten Techniken auf den Embedded-Systems-Bereich angepasst, um z.B. im Automobilbereich Anwendung zu finden. Ferner dient das Projekt zur Etablierung einer dauerhaften Kooperation zwischen der TU München und der NASA JPL.

Abschlussbericht
Ziel des Projektes Runtime-Verification war es, sich in die primär bei der NASA entwickelten Runtime-Verification-Techniken einzuarbeiten und diese in die Anwendungsdomäne der eingebetteten Systeme zu transferieren. In Besuchen am NASA Jet Propulsion Laboratory (JPL) wurde dabei intensiv mit Dr. Klaus Havelund zusammengearbeitet, um einerseits die aktuellen Techniken aufzuarbeiten und andererseits diese weiter zu entwickeln. Als Konsequenz aus dieser Zusammenarbeit ergab sich, dass eine präzise semantische Grundlage für Runtime-Verification-Ansätze zu erarbeiten ist. Ergebnisse dieser sich anschließenden Arbeit sind in [1-3] zu finden.

In 2011 führten Dr. Klaus Havelund und Dr. Martin Leucker ein gemeinsames Tutorial zum Thema Runtime-Verification auf der Konferenz Software Engineering and Formal Methods (SEFM'11, November 7-18, 2011, Montevideo, Uruguay) durch.

In den Diskussionen ergab sich ferner, dass neben der reinen Verifikation insbesondere auch die Diagnose von eingebetteten Systemen im Falle von erkannten Fehlern eine wichtige Forschungsfrage darstellt. Daher wurde ein Dagstuhl-Seminar zum Thema Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems zusammen mit Martin Sachenbacher, Oleg Sokolsky und Brian Williams beantragt, welches genehmigt und durchgeführt wurde (http://drops.dagstuhl.de/opus/volltexte/2011/2947/).

Referenzen:

[1] Bauer, Andreas, Leucker, Martin, and Schallhart, Christian. The good, the bad, and the ugly –but how ugly is ugly? Technical Report TUM-I0803, TU München, 2008.

[2] Dong, Wei, Leucker, Martin, and Schallhart, Christian. Impartial Anticipation in Runtime Verification. In Moonzoo Kim and Mahesh Viswanathan (editors), Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08), volume 5311, Lecture Notes in Computer Science, Springer, 2008.

[3] Leucker, Martin. Teaching Runtime Verification. Runtime Verification - Second International Conference, RV 2011, San Francisco, CA, USA, September 27-30, 2011, Revised Selected Papers, 2012.