Monitoring with Parameters

Abstract

Runtime monitoring of embedded systems is a method to safeguard their reliable operation by detecting runtime failures within the system and recognizing unexpected environment behavior during system development and operation. Specification languages for runtime monitoring aim to provide the succinct, understandable, and formal specification of system and component properties. Starting from temporal logics, this thesis extends the expressivity of specification languages for runtime monitoring in three key aspects while maintaining the predictability of resource usage. First, we provide monitoring algorithms for linear-time temporal logic with parameters (PLTL), where the parameters bound the number of steps until an eventuality is satisfied. Second, we introduce Lola 2.0, which adds data parameterization to the stream specification language Lola. Third, we integrate real-time specifications in RTLola and add real-time sliding windows, which aggregate data over real-time intervals. For the combination of these extensions, we present a design-time specification analysis which provides resource guarantees. We report on a case study on the application of the language in an autonomous UAS. Component and system properties were specified together with domain experts in the developed stream specification language and evaluated in a real-time hardware-in-the-loop testbed with a complex environment simulation.

Laufzeitüberwachung von eingebetteten Systemen ist eine Methode zur Absicherung zuverlässigen Systemverhaltens von Fehlern innerhalb des Systems und seiner Umgebung. Spezifikationssprachen zur Laufzeitüberwachung ermöglichen die kompakte, verständliche und formale Spezifikation von Eigenschaften auf Komponenten- und Systemebene. Beginnend bei temporalen Logiken, erweitert diese Dissertation die Ausdrucksfähigkeit von Spezifikationssprachen zur Laufzeitüberwachung in drei Kernaspekten, während die Vorhersagbarkeit von Ressourcennutzung erhalten bleibt. Erstens werden Algorithmen zur Überwachung mittels linear temporaler Logik mit Parametern (PLTL) beschrieben, wobei die Parameter die Einhaltung von Schrittgrenzen modaler Operatoren repräsentieren. Zweitens wird Lola 2.0 eingeführt, eine Erweiterung von Lola mit Datenparametern. Drittens wird gezeigt, wie Realzeitanforderungen in RTLola mittels gleitenden Fenstern über Realzeitintervallen integriert werden können. Für die Kombination aus diesen Erweiterungen wird eine Spezifikationsanalysetechnik aufgezeigt, welche zum Entwicklungszeitpunkt der Spezifikationen Garantien über die Ressourcennutzung zulässt. In einer praktischen Fallstudie wurde die praktische Anwendung der entwickelten Spezifikationssprachen zur Überwachung unbemannter autonomer Flugsysteme eingesetzt. Spezifikationen auf Komponenten- und Systemebene wurden in den entwickelten Spezifikationssprachen mit Domänenexperten entwickelt und auf einem echtzeitfähigen Prüfstand mit Umgebungssimulation erprobt.