Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-1001
Main Title: An Algorithm for the Real-Time Evaluation of Temporal Trace Specifications
Translated Title: Ein Algorithmus für die Realzeit-Auswertung Temporaler Verhaltensspezifikationen
Author(s): Lepper, Markus
Advisor(s): Pepper, Peter
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: Diese Arbeit präsentiert und diskutiert einen Algorithmus, der das Verhalten eines beliebigen dynamischen Systems (= "System Under Test" = "SUT") mit einer Spezifikation vergleicht, die eine Menge von erlaubten Verhaltensweisen beschreibt. Der Algorithmus wird definiert durch eine rein funktionale mathematische Darstellung, und seine Vollständigkeit, Korrektheit, Terminierung und Konfluenz werden bewiesen. Der Algorithmus arbeitet in Realzeit, insofern als er gleichzeitig mit dem SUT ausgeführt wird, und zu jedem Zeitpunkt ein Verdikt liefert, ob das Verhalten des SUT bis jetzt eine Erfüllung der Spezifikation noch erlaubt oder gar bereits impliziert. Die Spezifikationen werden in einer eigenen, aber durchaus kanonischen Sprache erstellt, welche die bekannte Syntax und Semantik von regulären Ausdrücken erweitert um die konjunktive Verknüpfung und um die Bedingungen bezgl. minimaler und maximaler Dauer von Unterausdrücken. Ein Spezifikationsausdruck beschreibt eine Menge von erlaubten Verhaltensweisen unmittelbar, insofern als eine syntaktische Folge von Unterausdrücken direkt der zeitlichen Abfolge von Unterabschnitten des Verhaltens entspricht. Die Ausdrucksfähigkeit der Spezifikationssprache entspricht einer temporalen Intervallogik zuzüglich Dauernanforderungen als "first class residents", aber ohne Negation. Die Grundlage ihrer Semantik und der Arbeitsweise des Algorithmus ist die Arithmetik von Intervallen über den reelen Zahlen R. Der Algorithmus bedarf, um auf ein beliebiges System angewandt zu werden, der Implementierung einer jeweils entsprechenden Adaptiven Schicht. Die Anforderungen an diese werden in der Arbeit spezifiziert. Der Algorithmus ist Kernbestandteil des im industriellen Kontext entwickelten Werkzeugs "MWatch", welches als Bibliotheksbaustein für die "matlab/simulink"-Umgebung implementiert ist, und für die Auswertung von Testdaten eingesetzt werden soll. Darüber hinaus enthält das Werkzeug eine Instanz der Adaptiven Schicht, welche im Haupttext erläutert wird, und realisiert eine programmierbare und zwei graphische Benutzerschnittstellen, welche in den als Anhang beigefügten Handbüchern beschrieben werden.
The thesis presents, discusses and proves the correctness of an algorithm which compares the behaviour of an arbitrarily defined dynamic system with a specification which describes a set of permitted behaviours. The algorithm is presented by pure mathematical functions, and its correctness, completeness and termination are proved. The specification is given as an expression from a corresponding specification language. The expressiveness of this language is that of a temporal interval logic over a dense domain, including duration specifications as first class residents, and excluding negation. The basis of its semantics, and of the operation of the algorithm, is the arithmetic on intervals from the real numbers. The algorithm works in real-time : while monitoring the growing prefix of the known behaviour of the system, it frequently generates verdicts indicating whether the complete behaviour of the SUT will finally fulfill or violate the specification, or whether this is currently still inconclusive. The real-time instant, when the algorithm's execution starts, serves as reference point for the semantics of the specification. An ending time instant of the SUT's behaviour may or may not be given, i.e. the algorithm can monitor finite or infinite real-time intervals of execution. Any kind of system can be monitored by the algorithm, if an "adaptive layer" is provided which transforms the observation data into the required input format. Currently both, the algorithm and an instance of this adaptive layer, are implemented in the "MWatch" tool. This tool is realized as a so-called "function block" in the matlab/simulink environment.
URI: urn:nbn:de:kobv:83-opus-9016
http://depositonce.tu-berlin.de/handle/11303/1298
http://dx.doi.org/10.14279/depositonce-1001
Exam Date: 29-Jun-2004
Issue Date: 4-Oct-2004
Date Available: 4-Oct-2004
DDC Class: 004 Datenverarbeitung; Informatik
Subject(s): Formale Methoden
Laufsemantik
Matlab
MWatch
Realzeit
Simulink
Testdatenauswertung
Formal methods
Matlab
MWatch
Real-time
Simulink
Test data evaluation
Trace semantics
Usage rights: Terms of German Copyright Law
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Publications

Files in This Item:
File Description SizeFormat 
Dokument_8.pdf1.53 MBAdobe PDFThumbnail
View/Open


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