Zeitdiagramme sind zur informellen Beschreibung von Hardwareprotokollen überaus nützlich; darum sind sie auch bei Hardware-Entwicklern sehr verbreitet. Eine Schwierigkeit von Zeitdiagrammen ist jedoch, daß ihre Semantik nicht mathematisch exakt gefaßt ist, so daß damit keine formalen Überprüfungen eines Protokolls möglich sind. Die hier vorgestellte Methodik des sog. Trigger-Graphen verwendet eine Zeitdiagramm-ähnliche Notation, die jedoch formal definiert ist. Mit dem Trigger-Graphen wird es möglich, Hardwareprotokolle auf eine Reihe von wichtigen Eigenschaften wie Vollständigkeit und Konsistenz zu überprüfen. Weiterhin kann man damit eine Transformation in Petri-Netze formulieren, so daß die dafür entwickelten Methoden auch für die Überprüfung von Hardwareprotokollen - z.B. auf die Einhaltung von Sicherheitsbedingungen - genutzt werden können. Die Trigger-Graph-Methodik wird an drei Beispielen erläutert: an einer Ampelsteuerung, einer Bahnschrankensteuerung und an einem DRAM-Leseprotokoll.
Formale Beschreibung und Verifikation von Hardwareprotokollen
Formal description and verification of hardware protocols
1995
19 Seiten, 11 Bilder, 2 Tabellen, 4 Quellen
Aufsatz (Konferenz)
Deutsch
Absicherung sicherheitskritischer Systeme - formale Verifikation
Kraftfahrwesen | 2009
|Formale Verifikation von Spezifikations-Modellen
Tema Archiv | 2001
|Formale Verifikation - eine leistungsfaehige Methodik zur Verifikation von embedded systemen
Kraftfahrwesen | 2002
|Formale Analyse und Verifikation von Statemate-Entwürfen
IuD Bahn | 2001
|Formale Verifikation einer Hardware-Implementierung des LIN-Protokoll Kontrollers
Tema Archiv | 2008
|