Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage RV-Techniken zur Analyse komplexer Systeme vor der Systembereitstellung, zu Test-, Verifizierungs- und Debugging-Zwecken sowie nach der Bereitstellung anwenden, um Zuverlässigkeit, Sicherheit, Robustheit und Sicherheit zu gewährleisten.

RV is a lightweight, yet rigorous, formal method that complements classical exhaustive verification techniques (such as model checking and theorem proving) with a more practical approach that analyses a single execution trace of a system. At the price of a limited execution coverage, RV can give very precise information on the runtime behaviour of the monitored system. The system considered can be a software system, hardware or cyber-physical system, a sensor network, or any system in general whose dynamic behaviour can be observed. The archetypal analysis that can be performed on runtime behaviour is to check for correctness of that behaviour. However, there are many other analyses (e.g., falsification analysis) or activities (e.g., runtime enforcement) that can be performed that are based on this techique. RV is now widely employed in both academia and industry both before system deployment, for testing, verification, and debugging purposes, and after deployment to ensure reliability, safety, robustness and security.

The course will start with an introduction on the areas where the verification should be preferable addressed at runtime. We will then explore different specification languages to specify the properties to be monitored and the related available monitoring techniques. We will then consider various instrumentation approaches can be used to extract the information necessary for monitoring from a running system. We will discuss some techniques of software system instrumentation. Real case studies will expose students to the potential applications of these technologies. A final project will give them the possibility to make a concrete experience of the concepts taught. This is the list of the main topics of the course:

1. Introduction to Runtime Verification
2. Specifying (Un)Desired System Behaviour
3. Generating Monitors from Formal Specifications
4. Instrumentation Techniques and Examples
5. Advance Topics: Specification-based Monitoring of Cyber-Physical Systems
6. Advance Topics: Fault-Localization and Fault Explanation
7. Advance Topics: Mining Specifications from Data
8. Advance Topics: From Runtime Verification to Control

In the first month of the course we will present the basic knowledge that is required to do the assignment. In the second part of the course, we will present advance topics that will be useful to further improve their project. We will ask the students to setup a git hub repository where we will monitor the progress and the actual work of the single students in the group. The students will ask to make two presentations. One presentation where the students must to elaborate, before starting the project, a contingency plan where they can still safely achieve some goals and the risk is
taken into consideration. The students must write a document explaining the solution adopted for their assignment. At end of the course, the students are asked to make a public final presentation where they  their results.

A project will be assigned to each student.  At the end of the semester the students will defend their solution in a public presentation.