Förderbeginn 01.07.2010

Runtime Reflection

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

Dr. Johan de Kleer
Palo Alto Research Center (PARC)
Intelligent Systems Lab



Runtime-Verification ist eine einfache aber effektive Verifikationstechnik, um Fehler in einem System zu erkennen. Die Entdeckung eines Fehlers gibt jedoch selten Auskunft über die Ursache eines Fehlers, geschweige denn darüber, was zu tun ist, um den Fehler zu beseitigen. Diagnose- und Planungstechniken erscheinen geeignet, diese Rolle übernehmen zu können. In diesem Forschungsprojekt wird Runtime-Reflection, ein Konzept des TUM-Teams, entwickelt, welches Runtime-Verification mit Diagnose- und Planungstechniken verbindet, um ein formal-fundiertes und gleichzeitig praxistaugliches Framework für die Fehlererkennung, Fehlerursachenerkennung und die Fehlerbehandlung für reaktive Systeme zu haben. In dem Projekt werden die Expertisen des TUM-Teams im Bereich der Runtime-Verification und die des PARC-Teams im Bereich der Diagnose und Planung kombiniert.

Abschlussbericht
Ziel des Projektes war es, Diagnosetechniken mit Runtime-Verification zu kombinieren, um neben der Fehlererkennung auch eine Fehlerlokalisation zu ermöglichen. Ferner war das Ziel, sich in die Fehlerbehandlung für reaktive Systeme einzuarbeiten, damit neben der Fehlerlokalisierung auch eine automatische Fehlerbehebung prinzipiell durchführbar ist. Im Rahmen eines Besuches von Johan de Kleer wurde intensiv der State-of-the-Art im Bereich der Diagnose erarbeitet. Im Zusammenhang mit einem Dagstuhl-Seminar (Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems) wurde die Thematik intensiv diskutiert und weiter verfolgt ( http://drops.dagstuhl.de/opus/volltexte/2011/2947/).

In Besuchen am Palo Alto Research Center (PARC) wurden ferner den dortigen Teilnehmern die neueren Erkenntnisse im Bereich der Runtime-Verification dargebracht [1-3], um die beiden Techniken zu kombinieren.

Es ist mittlerweile geplant, die Techniken im Bereich von Sensornetzwerken anzuwenden [4].

Referenzen:

[1] Leucker, Martin, and Schallhart, Christian. A Brief Account of Runtime Verification. Journal of Logic and Algebraic Programming, 78:293-303, 2009.

[2] Bauer, Andreas, Leucker, Martin, and Schallhart, Christian. Comparing LTL Semantics for Runtime Verification. Journal of Logic and Computation, 20:651–674, 2010.

[3] Bauer, Andreas, Leucker, Martin, and Schallhart, Christian. Runtime Verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM), 20(4):14, 2011.

[4] Fischer, Stefan, and Leucker, Martin. Runtime Verification and Reflection for Wireless Sensor Networks, SESENA, 2013.