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.2008
Runtime Verification - From Aeronautics to Automotive
PD Dr. Martin Leucker
Technische Universität München
Dr. Klaus Havelund
Laboratory for Reliable Software
Runtime verification is a lightweight verification technique
complementing traditional verification techniques such as model
checking and testing. One of the main distinguishing features of
runtime verification is due to its nature of being performed at
runtime: This opens up the possibility not only to detect incorrect
behavior of a software system but to react whenever misbehavior is
encountered. The proposed research cooperation aims at extending the
state-of-art of runtime verification and at extending the practical
applicability of runtime verification techniques beyond the aeronautic
sector to make it easily applicable for the embedded systems world as
found for example in the automotive sector. Moreover, a long term
collaboration in the field of runtime verification and related areas
of TUM and NASA JPL should be established.
Final report:
The goal of the project was to get acquainted with the runtime verification techniques that have primarily been developed at NASA with the aim to apply them in the area of embedded systems. During a visit at the NASA Jet Propulsion Laboratory (JPL) we worked intensively together with Dr. Klaus Havelund both for getting a coherent picture of the current work and to enhance the current state of the art. We identified that a precise formal semantics for runtime verification is necessary.
Corresponding results are [1-3].
In 2011 Dr. Klaus Havelund and Dr. Martin Leucker offered a joint tutorial on the topic of runtime verification at the Conference Software Engineering and Formal Methods (SEFM'11, November 7-18, 2011, Montevideo, Uruguay).
In further discussions we realized that plain verification for embedded systems should be extended by diagnosis to allow the localization of errors on top of their detection. Therefore we applied for a Dagstuhl Seminar on the topic of runtime verification, diagnosis, planning and control for autonomous systems together with Martin Sachenbacher, Oleg Sokolsky, and Brian Williams which was subsequently accepted and held.
Refereneces:
[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.