The authors formalize the correctness of a real-time scheduler in a time-triggered architecture. Where previous research elaborated on real-time protocol correctness, they extend this work to gate-level hardware. This requires a sophisticated analysis of analog bit-level synchronization and message transmission. Their case-study is a concrete automotive bus controller (ABC). For a set of interconnected ABCs they formally prove at gate-level, that all ABCs are synchronized tight enough such that messages are broadcast correctly. Proofs have been carried out in the interactive theorem prover Isabelle/HOL using the NuSMV model checker. To the best of their knowledge, this is the first effort formally tackling scheduler correctness at gate-level.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal correctness of an automotive bus controller implementation at gate-level


    Weitere Titelangaben:

    Formale Richtigkeit einer Kraftfahrzeug-Buscontroller-Implementierung auf Gatterebene


    Beteiligte:
    Alkassar, Eyad (Autor:in) / Böhm, Peter (Autor:in) / Knapp, Steffen (Autor:in)


    Erscheinungsdatum :

    2008


    Format / Umfang :

    11 Seiten, 3 Bilder, 19 Quellen





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch




    Timing Correctness in Safety-Related Automotive Software

    Griessing, Alexander / Emberson, Paul / Zalman, Rafael | SAE Technical Papers | 2011


    Timing Correctness in Safety-Related Automotive Software

    Zalman, R. / Griessing, A. / Emberson, P. et al. | British Library Conference Proceedings | 2011


    Formal Analysis of the Structural Correctness of SLC Descriptions

    Choi, S. J. / Scacchi, W. | British Library Online Contents | 2003


    Formal Analysis of Human Automation Interaction: The Problem of Display Correctness

    Degani, Asaf / Heymann, Michael / Austin, David et al. | NTRS | 1998