Please use this identifier to cite or link to this item: doi:10.22028/D291-28005
Title: Monitoring with Parameters
Author(s): Faymonville, Peter
Language: English
Year of Publication: 2019
SWD key words: Spezifikation
Parameter <Mathematik>
Verifikation
Free key words: Monitoring
Laufzeitüberwachung
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
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.
Link to this record: urn:nbn:de:bsz:291--ds-280054
hdl:20.500.11880/27458
http://dx.doi.org/10.22028/D291-28005
Advisor: Finkbeiner, Bernd
Date of oral examination: 17-May-2019
Date of registration: 17-Jun-2019
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
thesis-faymonville.pdfDissertation1,54 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.