h1

h2

h3

h4

h5
h6
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png

Temporal assertions for sequential and concurrent programs = Temporale Zusicherungen für Sequentielle und Nebenläufige Programme



Verantwortlichkeitsangabevorgelegt von Volker Stolz

ImpressumAachen : Publikationsserver der RWTH Aachen University 2006

UmfangII, 133 S. : graph. Darst.


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

  1. Fachgruppe Informatik (120000)
  2. Lehr- und Forschungsgebiet Informatik 2 (Programmiersprachen und Verifikation) (121420)

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:
Download 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

 GO


OpenAccess

QR Code for this record

The record appears in these collections:
Document types > Theses > Ph.D. Theses
Faculty of Mathematics, Computer Science and Natural Sciences (Fac.1) > Department of Computer Science
Publication server / Open Access
Public records
Publications database
120000
121420

 Record created 2013-01-28, last modified 2022-04-22


Fulltext:
Download fulltext PDF
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)