Runtime Verification

Semester:

SS 2013

Modul:

CS4137

Lecturer:

Prof. Dr. Martin Leucker

Assistants:

Normann Decker

Overview

Runtime verification is the discipline of computer science that deals with the study, development, and application of those verification techniques that allow checking whether a run of a system under scrutiny (SUS) satisfies or violates a given correctness property. It is being pursued as a lightweight verification technique complementing verification techniques such as model checking and testing and establishes another trade-off point between these forces.

As considered the heart of runtime verification, the main focus of the RV course lies on synthesis procedures yielding monitors from high-level specifications. We outline several monitor synthesis procedures for Linear-time Temporal Logic (LTL). In general, two main approaches can be found for synthesizing monitoring code: Monitors may either be given in terms of an automaton, which is precomputed from a given correctness specification. Alternatively, the correctness specification may be taken directly and rewritten in a tableau-like fashion when monitoring the SUS. We give examples for both approaches.

Surveys

Martin Leucker, Christian Schallhart: A brief account of runtime verification. J. Log. Algebr. Program. 78(5): 293-303 (2009)
Martin Leucker: Teaching Runtime Verification. RV 2011: 34-48

Topics covered

Temporal logic and multi-valued semantics
Finite (ω-)automata
Monitor synthesis
- Automata constructions and -analysis
- Formula rewriting
Runtime monitoring, monitor integration
RV frameworks

SS 2013

Lecture
Tuesday July 9, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64) [cancelled]
Tuesday 10:15-11:45 0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64

Exercise
Wednesday 14:00-15:30 0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64 (not every week)

Lecture
Tuesday April 9, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday April 16, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday April 23, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday April 30, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday May 7, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday May 14, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday May 21, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday May 28, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday June 4, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday June 11, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday June 18, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday June 25, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday July 2, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Tuesday July 9, 2013 10:15-11:45 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64) [cancelled]

Exercise
Wednesday April 17, 2013 14:00-15:30 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Wednesday May 8, 2013 14:00-15:30 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Wednesday May 22, 2013 14:00-15:30 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Wednesday June 5, 2013 14:00-15:30 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Wednesday June 19, 2013 14:00-15:30 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)
Wednesday July 3, 2013 14:00-15:30 (0.068/0.069 (Seminarraum Informatik 3/2, Karp/Cook), Building 64)

click to view Dates.

Lectures

Lectures start on April 9, 2013 and will be held on a week basis on Tuesdays, 10.15 - 11.45.

Exercises

Exercise problems will be made available on this web page and handed out during the lectures. We will discuss the problems roughly every two weeks, starting on April 17, 2013. Beware of the shift due to holiday on May 1st. See dates above.

We strongly encourage participants to work on the exercise problems and hand in (even incomplete) solutions for review before their discussion. Also, feel free to contact Normann and request discussion/repetition of certain topics if needed.

Mailing list

Important information related to the course Runtime Verification will be distributed through the mailing list. Attendees are strongly encouraged to register with the list. Note that access is only possible from inside the domain uni-luebeck.de.

Mailing list Runtime Verification

Module

Information on the Module CS4137 Runtime Verification (RV)

Examination

Depending on the number of participants, there will be an oral or written exam. For oral exams please contact Hedwig Hellkamp.

Topics from both, lectures and exercises, will be subject to examination. We therefor strongly recommend to follow the lectures the exercises.

Material