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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formale Verifikation einer Hardware-Implementierung des LIN-Protokoll Kontrollers


    Weitere Titelangaben:

    Formal verification of a hardware implementation of the LIN protocol controller


    Beteiligte:


    Erscheinungsdatum :

    2008


    Format / Umfang :

    10 Seiten, 2 Bilder, 3 Tabellen, 10 Quellen



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Deutsch




    Absicherung sicherheitskritischer Systeme - formale Verifikation

    Tchernikov,M. / Swaminathan,M. | Kraftfahrwesen | 2009



    Formale Verifikation - eine leistungsfaehige Methodik zur Verifikation von embedded systemen

    Sperling,T. / Esterel Technologies,Ottobrunn,DE | Kraftfahrwesen | 2002