Stream-based Runtime Verification (Tutorial @ FM Week, 11. Oct. 2019)

Tutorial at FM Week 2019, 11. Oct. 2019, Porto/Portugal (venue/registration info)

Runtime verification (RV) is a light-weight verification technique for online monitoring a particular execution of the system under test. While traditional RV approaches use temporal logics, Stream-based Runtime Verification (SRV) extends RV with the concept of complex event processing. SRV is not limited to verification of correct executions, but also allows to specify quantitative and statistical analyses of program traces. We present synchronous and asynchronous SRV languages, i.e. LOLA and the temporal stream-based specification language TeSSLa. After establishing the theoretical foundations we present software- and hardware-based implementations of SRV and compare them to other hardware-based RV~approaches. In this tutorial we consider cyber-physical systems (CPS) as an example application. We demonstrate how to use SRV to integrate continuous and discrete signals from different trace source of a CPS. We present a comprehensive approach to non-intrusive monitoring of multi-core processors using SRV. We demonstrate how embedded trace-ports of multi-core processors can be used to access the actual control flow trace executed by the program running on the processor. We carry out analyses on the control flow trace of typical cyber-physical systems in real time using FPGAs. We describe how light-weight, hardware-supported instrumentation can be used to enrich the control-flow trace with data values from the application. Finally, we demonstrate how these technologies can be used to detect data races in cyber-physical systems.

Topics

  • TeSSLa: Temporal Stream-based Specification Language (https://www.tessla.io)
  • Hardware-assisted runtime verification with FPGAs in the COEMS project
  • Data-race detection with the COEMS-tools

 

Agenda COEMS Tutorial @ FM

09:00Practical Demonstration
(Daniel Thoma, University of Lübeck, Germany)
10:00Coffee Break
10:30Introduction to Stream-based Runtime Verification
(César Sánchez, IMDEA Software Institute, Spain)
11:30Introduction to TeSSLa - Temporal Stream-based Specification Language
(Hannes Kallwies, University of Lübeck)
12:30Lunch Break
14:00TeSSLa in Practice
(Malte Schmitz, University of Lübeck)
15:30Coffee Break
16:00In-depth Application: Data Races
(Volker Stolz, Høgskulen på Vestlandet, Norway)
Future Prospect
(Martin Leucker, University of Lübeck)

 

Presenters

  • Martin Leucker (University of Lübeck, Germany)
  • César Sánchez (IMDEA Software Institute, Spain)
  • Volker Stolz (Høgskulen på Vestlandet, Norway)
  • Malte Schmitz (University of Lübeck, Germany)
  • Daniel Thoma (University of Lübeck, Germany),