Runtime Verification and Testing

+++ Please register on the Moodle page. Any further updates on the course will only be published on that Moodle page. +++

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 behaviors 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 in 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 of 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