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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

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


    Weitere Titelangaben:

    Using formal methods in designing embedded systems for automotive applications


    Beteiligte:
    Damm, W. (Autor:in) / Eckrich, M. (Autor:in) / Brockmaeyer, U. (Autor:in) / Wiottich, G. (Autor:in) / Holberg, H.J. (Autor:in)


    Erscheinungsdatum :

    1997


    Format / Umfang :

    18 Seiten, 8 Bilder, 16 Quellen




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Deutsch