2006 & 2007
Aachen, Techn. Hochsch., Diss., 2006
Prüfungsjahr: 2006. - Publikationsjahr: 2007
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
Tag der mündlichen Prüfung/Habilitation
2006-07-20
Online
URN: urn:nbn:de:hbz:82-opus-19771
URL: https://publications.rwth-aachen.de/record/62419/files/Stolz_Volker.pdf
Einrichtungen
Inhaltliche Beschreibung (Schlagwörter)
Assertion (Genormte SW) ; Temporale Logik (Genormte SW) ; Informatik (frei) ; runtime verification (frei) ; temporal logic (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
In dieser Arbeit präsentieren wir eine Erweiterung des Konzepts der Assertion: Temporale Assertions erlauben die Spezifikation und Validierung temporaler Safety-Eigenschaften einer Anwendung zur Laufzeit. Wir sehen dies als notwendigen Schritt, um die wachsende Zahl impliziten Anforderungen an Software-Spezifikationen zu überprüfen, welche oft nur informell in der Dokumentation der Schnittstellen gegeben sind und nicht von Übersetzern oder Model Checkern überprüft werden können. Außerdem zeigen wir, wie unsere Technik auf existierende Programme angewandt werden kann, ohne den Quelltext zu verändern. Da wie auch mit Assertions unser Ansatz das Nichtvorhandensein von Fehlern nicht zeigen kann, gibt er dem Programmierer ein mächtigeres Werkzeug, Annahmen über sein Programm zur Laufzeit zu überprüfen.
In this thesis, we present an extension to the well-known concept of assertions: temporal assertions allow the specification and validation of modal safety properties of an application at runtime. We see this as a necessary step in enforcing the growing number of implicit requirements of software specifications, which are often only informally defined in the documentation of application program interfaces (API) and are beyond the reach of type checkers, compilers, or model checkers. Also, we show how our techniques can be applied to existing programs without modifying the source code. Although, like assertions, our approach cannot prove the absence of errors, it gives the programmer a more powerful means of automatically checking assumptions about his program at runtime.
Fulltext:
PDF
Dokumenttyp
Dissertation / PhD Thesis
Format
online, print
Sprache
English
Externe Identnummern
HBZ: HT015270498
Interne Identnummern
RWTH-CONV-123989
Datensatz-ID: 62419
Beteiligte Länder
Germany