Runtime Verification und Testen

Semester:

SS 2015

Modul:

CS4137 RV,

CS4136 Testen,

CS4139 RVTesten,

CS4139 T RVTestena

Lecturer:

Prof. Dr. Martin Leucker

Assistants:

Malte Schmitz

Overview

Software developers spend between 50% and 70% of the time testing and validating code. Testing code can be defined as the examination of a subset of the behaviours of the program or the system under test. The testing part of this course covers the different techniques and approaches to test software.

The main focus lies on computer-assisted unit testing. This field can be roughly separated into black-box testing where you do not have access to the code and white-box testing where test cases can be designed or generated from the code.

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.

This course treats how white-box testing and especially automated test case generation and runtime verification can be combined to a powerful verification method.

As considered the heart of runtime verification, the main focus of the RV part of the 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.

Topics Covered

Definitions of Testen, Verification and Validation
Static testing vs. Dynamic Testing
Manual vs. Automated Testing
Black box vs. White box Testing
Coverage Criteria
Test case generation
Temporal logic and multi-valued semantics
Finite (ω-)automata
Monitor synthesis
- Automata constructions and -analysis
- Formula rewriting
Runtime monitoring, monitor integration
RV frameworks
Conformance Testing

SS 2015

Lecture
Monday 12:15-13:45 V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik
Wednesday 10:15-11:45 Seminarraum Informatik 5 (Von Neumann) (not every week)

Exercise Group 1
Wednesday 10:15-11:45 Seminarraum Informatik 5 (Von Neumann) (not every week)

Exercise Group 2
Tuesday 12:15-13:45 Seminarraum IFIS 2035 (not every week)

Lecture
Monday April 13, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Wednesday April 15, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Monday April 20, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Monday April 27, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Wednesday April 29, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Monday May 4, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Monday May 11, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Wednesday May 13, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Monday May 18, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Monday May 25, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Wednesday May 27, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Monday June 1, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Monday June 8, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Wednesday June 10, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Monday June 15, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Monday June 22, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Wednesday June 24, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Monday June 29, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Monday July 6, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)
Wednesday July 8, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Monday July 13, 2015 12:15-13:45 (V 2 - Hörsaal V 2, Hörsaalgebäude Vorklinik)

Exercise Group 1
Wednesday April 22, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Wednesday May 6, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Wednesday May 20, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Wednesday June 3, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Wednesday June 17, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Wednesday July 1, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))
Wednesday July 15, 2015 10:15-11:45 (Seminarraum Informatik 5 (Von Neumann))

Exercise Group 2
Tuesday April 21, 2015 12:15-13:45 (Seminarraum IFIS 2035)
Tuesday May 5, 2015 12:15-13:45 (Seminarraum IFIS 2035)
Tuesday May 19, 2015 12:15-13:45 (Seminarraum IFIS 2035)
Tuesday June 2, 2015 12:15-13:45 (Seminarraum IFIS 2035)
Tuesday June 16, 2015 12:15-13:45 (Seminarraum IFIS 2035)
Tuesday June 30, 2015 12:15-13:45 (Seminarraum IFIS 2035)
Tuesday July 14, 2015 12:15-13:45 (Seminarraum IFIS 2035)

click to view Dates.

Lectures

Lectures start on April 13, 2015 and will be held on a week basis on Mondays, 12:15–13:45 and every other week on Wednesdays, 10:15–11:45. See dates above.

Exercises

Exercise problems will be made available on this web page and handed out during the lectures roughly every two weeks at least one week before their deadline. We will discuss the problems in the exercises directly after the deadline, starting on April 22, 2015. The exercises take place on the Wednesdays, 10:15–11:45, when no lecture is given. See dates above.

Solutions must be handed in before the exercise in which they will be discussed. You can hand in your solution alone or in groups of two students. Write your solutions in German or English language. You can hand in your solutions on paper or via email to Alexander and Moritz:

Alexander Schramm: alexander.schramm [at] student.uni-luebeck.de
Moritz Flucht: moritz.flucht [at] student.uni-luebeck.de

Ratings. Your solution of every task will be rated according to the following schema:
0 points: You didn't manage to hand in anything meaningful.
1 point: We honor your attempt, but it is mainly wrong.
2 points: Your solution is mainly correct.
3 points: Your solution is correct and nice.

To pass the exercises you need to achieve 1 point in every task on every exercise sheet. You can leave out one exercise sheet.

Also, feel free to contact Malte and request discussion/repetition of certain topics if needed.

Mailing list

Important information related to this course will be distributed through the mailing list. Attendees are strongly encouraged to register with the list. Note that access is only possible from inside our universities network or via the SSL gate.