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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formale Beschreibung und Verifikation von Hardwareprotokollen


    Additional title:

    Formal description and verification of hardware protocols


    Contributors:


    Publication date :

    1995


    Size :

    19 Seiten, 11 Bilder, 2 Tabellen, 4 Quellen



    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    German





    Absicherung sicherheitskritischer Systeme - formale Verifikation

    Tchernikov,M. / Swaminathan,M. | Automotive engineering | 2009


    Formale Verifikation - eine leistungsfaehige Methodik zur Verifikation von embedded systemen

    Sperling,T. / Esterel Technologies,Ottobrunn,DE | Automotive engineering | 2002



    Formale Verifikation einer Hardware-Implementierung des LIN-Protokoll Kontrollers

    Schmidt, Bernard / Bulach, Slava / Weinberger, Katharina et al. | Tema Archive | 2008