Schlör, Rainer C. (2002) Symbolic timing diagrams: a visual formalism for model verification. PhD, Universität Oldenburg.

Preview

- Accepted Version Volltext (2239Kb)

Abstract

The work described in this thesis introduces a novel visual specification formalism named STD which can be used to verify models of reactive systems. The presentation has three parts: First, an introduction and motivation is given. Second, a theoretical framework needed to describe the context of the design of STD is layed out. Third, the novel formalism itself is introduced in two steps: First, a syntactical subset (LSTD) of STD is analyzed in detail, and the semantics is illustrated by a representative set of derivation proof rules. Second, the main formalism STD is defined. The connection between LSTD and STD is established by a theorem, which shows that a STD specification can be represented by an equivalent LSTD specification. While the presentation is focused on the theoretical foundation of STD, complementary work has been performed over the past five years to bring the concept of STD to a usable implementation. This is shortly described in the first part of the thesis. The formalism has been integrated into existing verification frameworks for different specification languages, in particular for VHDL and the Statemate(TM) framework.

["eprint_fieldname_abstract_plus" not defined]

In der vorliegenden Arbeit wird eine neuartige visuelle Spezifikationstechnik mit der Bezeichnung STD (Symbolic Timing Diagrams) eingeführt und untersucht. Die Spezifikationstechnik wurde speziell für die Verifikation von Modellen eingebetteter Systeme entwickelt. Die Arbeit hat drei Teile: Zunächst wird eine Einführung und Motivation zur Verwendung von STD gegeben. Im zweiten Teil der Arbeit werden die theoretischen Werkzeuge und Begriffe eingeführt, auf deren Basis die Semantik von STD beruht. Der Formalismus STD wird in zwei Stufen eingeführt und erklärt: Zunächst wird eine syntaktische Untermenge von STD (mit der Bezeichung LSTD) analysiert, und das Verständnis der Semantik von LSTD durch die Vorstellung eines Satzes von Beweisregeln (Ableitungsregeln) unterstützt. Im zweiten Schritt wird der Hauptformalismus STD definiert. Der Zusammenhang zwischen LSTD und STD wird durch einen Hauptsatz hergestellt, der zeigt, dass sich jede STD Spezifikation in eine äquivalente LSTD Spezifikation überführen lässt. Obwohl die Arbeit sich auf die theoretischen Grundlagen von STD konzentriert, wurden zahlreiche ergänzende praktische Studien seit 1995 durchgeführt und das Konzept von STD bis zur Entwicklung eines in der Praxis anwendbaren Werkzeugsatzes fortgeführt. Dies wird kurz im ersten Teil der Arbeit beschrieben. Der Formalismus wurde in verschiedene Verifikationsumgebungen integriert, insbesondere für die bekannten Modellierungssprachen VHDL und Statemate(TM).

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	[Keine Schlagwörter von Autor/in vergeben.]
Controlled Keywords:	Eingebettete Systeme, Modell
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	17 Jan 2013 14:16
Last Modified:	05 Dec 2013 14:45
URI:	https://oops.uni-oldenburg.de/id/eprint/301
URN:	urn:nbn:de:gbv:715-oops-3312
DOI:
Nutzungslizenz:

Actions (login required)

View Item