In der Automobilindustrie werden häufig Bussysteme für die Kommunikation zwischen Fahrzeugkomponenten eingesetzt. Gerade in einem solchen Einsatzbereich mit diversen sicherheitskritischen Anwendungen ist es wichtig, Hardwareentwürfe best möglich zu verifizieren. Dazu bieten sich formale Methoden an. Üblicherweise werden bei der formalen Verifikation zunächst einzelne Blöcke auf der Modulebene verifiziert und anschließend die Kommunikation der Module untereinander überprüft. Dazu ist es zunächst notwendig, die Kommunikationsschnittstellen, die Protokolle, zwischen den Modulen zu verifizieren. Es wird anhand einer LIN-Slave-Implementierung untersucht, ob es möglich ist, eine Formale Verifikation mittels Interval Property Checking auf Protokollebene durchzuführen. Dabei entstand das hier vorgestellte Greybox-Verfahren, bei dem die Protokolltransaktionen in einzelne Abschnitte zerlegt werden, so dass diese auf der vollständigen Hardware-Implementierung überprüft werden können. Es wird auch der Beweis erbracht, dass die Protokollabschnitte in korrekter Reihenfolge aufeinander folgen. Des weiteren wird gezeigt, wie durch Verkettung der Abschnitte die vollständige Überprüfung ganzer Transaktionen in greifbare Nähe rückt. Das Ziel das hier verfolgt wird, ist ein höchst möglicher Grad an Unabhängigkeit der Eigenschaften von internen Signalen des Entwurfs zu erreichen. Dadurch können die beschriebenen Eigenschaften für unterschiedliche Implementierungen zur formalen Verifikation genutzt werden.
Formale Verifikation einer Hardware-Implementierung des LIN-Protokoll Kontrollers
Formal verification of a hardware implementation of the LIN protocol controller
2008
10 Seiten, 2 Bilder, 3 Tabellen, 10 Quellen
Aufsatz (Konferenz)
Deutsch
Absicherung sicherheitskritischer Systeme - formale Verifikation
Kraftfahrwesen | 2009
|Formale Verifikation von Spezifikations-Modellen
Tema Archiv | 2001
|Formale Verifikation - eine leistungsfaehige Methodik zur Verifikation von embedded systemen
Kraftfahrwesen | 2002
|Formale Beschreibung und Verifikation von Hardwareprotokollen
Tema Archiv | 1995
|Formale Analyse und Verifikation von Statemate-Entwürfen
IuD Bahn | 2001
|