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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formale Verifikation einer Hardware-Implementierung des LIN-Protokoll Kontrollers


    Additional title:

    Formal verification of a hardware implementation of the LIN protocol controller


    Contributors:


    Publication date :

    2008


    Size :

    10 Seiten, 2 Bilder, 3 Tabellen, 10 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