Es wird Einblick gegeben in die Technik des Modelcheckings zu formalen Verifikation von Verhaltenseigenschaften, sog. Lebendigkeits- und Sicherheitseigenschaften einer Funktionslogik mit rein diskret reaktivem Verhalten, wie sie typischerweise in eingebetteten Systemen, wie z.B. Steuerungssystemen im Automobil ihren Einsatz findet. Der dazu notwendige Werkzeugverbund wird im Überblick vorgestellt. Anhand der Fallstudie Kfz-Zentralverriegelung wird zum einen eine Einführung in den Formalismus der State-Sharts gegeben, sowie eine dazu geeignete Methodik zur Funktionsspezifikation aufgezeigt, zum anderen der Formalismus der Symbolischen Zeitdiagramme zur Spezifikation von sicherheitskritischen Anforderungen an das Verhalten der Funktionslogik erläutert. Schließlich wird das Ergebnis der Verifikation einiger ausgewählter Eigenschaften einer Zentralveriegelungskomponente präsentiert. Anhand der Einordnung des Modelcheckings speziell im BMW-Entwurfsprozeß werden die Notwendig dessen Einsatzes sowie die damit verbundenen Vorteile für die Produktentwicklung identifiziert.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Einsatz formaler Methoden zur Erhöhung der Sicherheit eingebetteter Systeme im Kfz


    Additional title:

    Using formal methods in designing embedded systems for automotive applications


    Contributors:
    Damm, W. (author) / Eckrich, M. (author) / Brockmaeyer, U. (author) / Wiottich, G. (author) / Holberg, H.J. (author)


    Publication date :

    1997


    Size :

    18 Seiten, 8 Bilder, 16 Quellen




    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    German