Spezifikation und Generierung von zeitlich-logischen Eigenschaftssätzen aus Sequenzdiagrammen
Autoren
Parameter
Mehr zum Buch
Zwei wesentliche Anforderungen an den Entwicklungsprozess von modernen integrierten Schaltungen sind eine kurze Entwicklungszeit und Fehlerfreiheit. Einen Beitrag zur Erfüllung dieser Anforderungen leistet hierfür der Aufbau von Schaltungsentwürfen aus Komponenten, die jeweils auf eine Funktion spezialisiert sind und für die bereits fertige Entwürfe vorliegen. Diese Komponenten kommunizieren auf dem fertigen Chip untereinander. Wenn Schaltungsbestandteile für die Kommunikation fehlerhaft implementiert wurden, funktioniert der Chip nicht richtig. Weil die Fehlersuche heutzutage einen großen Teil der gesamten Entwicklungszeit ausmacht ist eine möglichst effiziente Herangehensweise unverzichtbar. In den letzten Jahren hat die formale Verifikation dabei an Bedeutung hinzugewonnen. Für die Fehlersuche ist es notwendig, dass die Spezifikation, die normalerweise in umgangssprachlicher Form vorliegt, in eine maschinenlesbare Form gebracht wird. Für diesen Zweck existieren formale Sprachen, die Eigenschaftsbeschreibungssprachen (z. B. PSL oder SVA). In diesen Sprachen werden zeitlich-logische Eigenschaften (engl: Assertions) der Komponenten oder des Systems spezifiziert, die von der tatsächlichen Implementierung erfüllt werden müssen. In dieser Arbeit werden Sequenzdiagramme benutzt, um den funktionalen Teil einer Systemspezifikation graphisch darzustellen. Sequenzdiagramme sind besonders geeignet für die Darstellung von Kommunikationsverhalten und lassen sich deshalb gut für die formale Spezifikation von Halbleiterschaltungen einsetzen. Ein weiterer Vorteil ist, dass Sequenzdiagramme als allgemein gut lesbar angesehen werden, speziell auch von Personen ohne vertiefte technische Kenntnisse. Um die in Form von Sequenzdiagrammen vorliegende Spezifikation gegen eine Implementierung verifizieren zu können, werden Sequenzdiagramme in formale Eigenschaften übersetzt. Aus einem Sequenzdiagramm lassen sich Eigenschaften für alle beteiligten Komponenten generieren, so dass dieses nur einmal für das gesamte System erstellt werden müssen. Es lassen sich sowohl Monitoreigenschaften als auch Transaktionseigenschaften erzeugen. Die Besonderheit des in dieser Arbeit vorgestellten Verfahrens ist die Spezifikation des Systemverhaltens mit Sequenzdiagrammen auf der hardwarenahen Registertransferebene. Hierfür wird zunächst eine spezielle Interpretationsweise für Sequenzdiagramme festgelegt. Die Anwendbarkeit des Ansatzes wird an Beispielen demonstriert.
Buchkauf
Spezifikation und Generierung von zeitlich-logischen Eigenschaftssätzen aus Sequenzdiagrammen, Martin Schweikert
- Sprache
- Erscheinungsdatum
- 2012
Lieferung
Zahlungsmethoden
Feedback senden
- Titel
- Spezifikation und Generierung von zeitlich-logischen Eigenschaftssätzen aus Sequenzdiagrammen
- Sprache
- Deutsch
- Autor*innen
- Martin Schweikert
- Verlag
- dissertation.de
- Erscheinungsdatum
- 2012
- ISBN10
- 3866245718
- ISBN13
- 9783866245716
- Reihe
- Dissertation.de
- Kategorie
- Skripten & Universitätslehrbücher
- Beschreibung
- Zwei wesentliche Anforderungen an den Entwicklungsprozess von modernen integrierten Schaltungen sind eine kurze Entwicklungszeit und Fehlerfreiheit. Einen Beitrag zur Erfüllung dieser Anforderungen leistet hierfür der Aufbau von Schaltungsentwürfen aus Komponenten, die jeweils auf eine Funktion spezialisiert sind und für die bereits fertige Entwürfe vorliegen. Diese Komponenten kommunizieren auf dem fertigen Chip untereinander. Wenn Schaltungsbestandteile für die Kommunikation fehlerhaft implementiert wurden, funktioniert der Chip nicht richtig. Weil die Fehlersuche heutzutage einen großen Teil der gesamten Entwicklungszeit ausmacht ist eine möglichst effiziente Herangehensweise unverzichtbar. In den letzten Jahren hat die formale Verifikation dabei an Bedeutung hinzugewonnen. Für die Fehlersuche ist es notwendig, dass die Spezifikation, die normalerweise in umgangssprachlicher Form vorliegt, in eine maschinenlesbare Form gebracht wird. Für diesen Zweck existieren formale Sprachen, die Eigenschaftsbeschreibungssprachen (z. B. PSL oder SVA). In diesen Sprachen werden zeitlich-logische Eigenschaften (engl: Assertions) der Komponenten oder des Systems spezifiziert, die von der tatsächlichen Implementierung erfüllt werden müssen. In dieser Arbeit werden Sequenzdiagramme benutzt, um den funktionalen Teil einer Systemspezifikation graphisch darzustellen. Sequenzdiagramme sind besonders geeignet für die Darstellung von Kommunikationsverhalten und lassen sich deshalb gut für die formale Spezifikation von Halbleiterschaltungen einsetzen. Ein weiterer Vorteil ist, dass Sequenzdiagramme als allgemein gut lesbar angesehen werden, speziell auch von Personen ohne vertiefte technische Kenntnisse. Um die in Form von Sequenzdiagrammen vorliegende Spezifikation gegen eine Implementierung verifizieren zu können, werden Sequenzdiagramme in formale Eigenschaften übersetzt. Aus einem Sequenzdiagramm lassen sich Eigenschaften für alle beteiligten Komponenten generieren, so dass dieses nur einmal für das gesamte System erstellt werden müssen. Es lassen sich sowohl Monitoreigenschaften als auch Transaktionseigenschaften erzeugen. Die Besonderheit des in dieser Arbeit vorgestellten Verfahrens ist die Spezifikation des Systemverhaltens mit Sequenzdiagrammen auf der hardwarenahen Registertransferebene. Hierfür wird zunächst eine spezielle Interpretationsweise für Sequenzdiagramme festgelegt. Die Anwendbarkeit des Ansatzes wird an Beispielen demonstriert.