191.118 Runtime Verification
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2020S, VU, 4.0h, 6.0EC
TUWEL

Merkmale

  • Semesterwochenstunden: 4.0
  • ECTS: 6.0
  • Typ: VU Vorlesung mit Übung

Lernergebnisse

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.

Inhalt der Lehrveranstaltung

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



Methoden

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.

Prüfungsmodus

Prüfungsimmanent

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Do.14:00 - 16:0012.03.2020 CPS Library (Treitlstrasse 1, 3rd Floor)Introduction (Dejan Nickovic)
Di.14:00 - 16:0017.03.2020 CPS Library (Treitlstrasse 1, 3rd Floor)Specification Languages/Monitoring Algorithms (1) (Dejan Nickovic)
Mi.14:00 - 16:0018.03.2020 CPS Library (Treitlstrasse 1, 3rd Floor)Specification Languages/Monitoring Algorithms (2) (Dejan Nickovic)
Di.14:00 - 16:0024.03.2020 CPS Library (Treitlstrasse 1, 3rd Floor)Specification Languages/Monitoring Algorithms (3) (Dejan Nickovic)
Mi.14:00 - 16:0025.03.2020 CPS Library (Treitlstrasse 1, 3rd Floor)RV Instrumentation (1) (Ezio Bartocci)
Di.14:00 - 16:0031.03.2020 CPS Library (Treitlstrasse 1, 3rd Floor)RV Instrumentation (2) (Ezio Bartocci)
Mi.14:00 - 16:0001.04.2020 CPS Library (Treitlstrasse 1, 3rd Floor)Falsification Analysis (Dejan Nickovic)
Di.14:00 - 16:0021.04.2020 CPS Library (Treitlstrasse 1, 3rd Floor)Trace Diagnostics/Failure Explanation (Dejan Nickovic)
Mi.14:00 - 16:0022.04.2020 CPS Library (Treitlstrasse 1, 3rd Floor)Specification Mining (Ezio Bartocci)
Di.14:00 - 16:0028.04.2020 CPS Library (Treitlstrasse 1, 3rd Floor)Spatio-Temporal Monitoring (Ezio Bartocci)
Mi.14:00 - 16:0029.04.2020 CPS Library (Treitlstrasse 1, 3rd Floor)From Runtime Verification to Runtime Control Synthesis (Ezio Bartocci)
Di.14:00 - 16:0005.05.2020 CPS Library (Treitlstrasse 1, 3rd Floor)Project Assignment (Ezio Bartocci)

Leistungsnachweis

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

LVA-Anmeldung

Von Bis Abmeldung bis
12.02.2020 23:59 03.03.2020 23:59

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Sprache

Englisch