Symbolic timing diagrams: a visual formalism for model verification

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.

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Oldenburg

Year

2001

Author dc:creator

• Schlör, Rainer C.

• [Keine Schlagwörter von Autor/in vergeben.]

Repository record source_url

http://oops.uni-oldenburg.de/301

OAI identifier oai:identifier

oai:oops.uni-oldenburg.de:301