Please select the desired project time frame:
- July 2026
- January 2026
- July 2025
- January 2025
- July 2024
- January 2024
- July 2023
- January 2023
- July 2022
- January 2022
- July 2021
- January 2021
- July 2020
- January 2020
- July 2019
- January 2019
- July 2018
- January 2018
- July 2017
- January 2017
- July 2016
- January 2016
- July 2015
- January 2015
- July 2014
- January 2014
- July 2013
- January 2013
- July 2012
- January 2012
- July 2011
- January 2011
- July 2010
- January 2010
- July 2009
- January 2009
- July 2008
- January 2008
- July 2007
- January 2007
- July 2006
- January 2006
- July 2005
- January 2005
- July 2004
- January 2004
- July 2003
- January 2003
- July 2002
- January 2002
- July 2001
- January 2001
Start of funding 01.07.2010
Runtime Reflection
PD Dr. Martin Leucker
Technische Universität München
Dr. Johan de Kleer
Palo Alto Research Center (PARC)
Intelligent Systems Lab
Runtime verification is a lightweight verification technique
complementing traditional verification techniques. It is well suited
for failure detection, i.e., for finding out whether a failure has
happened in a software system. However, then it is typically unclear
where a failure has happened and what to do to deal with the failure.
Diagnosis and planning, are promising techniques to address the
localization and healing of failures. This research project will
develop runtime reflection, a concept proposed by the TUM team, by
combining runtime verification, diagnosis, and planning towards a
formal yet practical method for failure detection, identification, and
reconfiguration (FDIR) of reactive systems. It combines the expertise
of the TUM team on runtime verification and that of the PARC team on
diagnosis and planning.
Final report:
The goal of the project was to combine runtime verification and diagnosis to allow not only the detection but also the identification of failures. A further goal of the project was to consider the existing work on failure mitigation to enable the automatic repair of failures, at least in general, in addition to the failure localization.
Johan de Kleer from Palo Alto Research Center was visiting us and we worked out the state of the art in the area of diagnosis. In a Dagstuhl Seminar (runtime verification diagnosis, planning and control for autonomous systems) we elaborated and enhanced these topics further.
During a visit at the Palo Alto Research Center (PARC) we reported on the new developments in the field of runtime verification to allow the combination of runtime verification and diagnosis.
Meanwhile we plan to apply these techniques in the area of sensor networks.
References:
[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.