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.
Einsatz formaler Methoden zur Erhöhung der Sicherheit eingebetteter Systeme im Kfz
Using formal methods in designing embedded systems for automotive applications
1997
18 Seiten, 8 Bilder, 16 Quellen
Conference paper
German
Einsatz formaler Methoden zur Erhoehung der Sicherheit eingebetteter Systeme im Kfz
Automotive engineering | 1998
|Sicherheit eingebetteter Systeme auf Basis arithmetischer Codierungen
Tema Archive | 2014
|Semiformale Methoden für den automatisierten Test eingebetteter Systeme
Tema Archive | 2007
|Zum Einsatz dynamisch rekonfigurierbarer eingebetteter Systeme in der Bildverarbeitung
Tema Archive | 2011
|