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). <dt.>
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. <engl.>
von Tom Bienmüller ; Udo Brockmeyer ; Werner Damm ; Gert Döhmen ; Claus Eßmann ; Hans Jürgen Holberg ; Hardi Hungar ; Bernhard Josko ; Rainer Schlör ; Gunnar Wittich ; Hartmut Wittke ; Geoffrey Clements ; John Rowlands ; Eric Sefton
