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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

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


    Additional title:

    Formale Richtigkeit einer Kraftfahrzeug-Buscontroller-Implementierung auf Gatterebene


    Contributors:


    Publication date :

    2008


    Size :

    11 Seiten, 3 Bilder, 19 Quellen





    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English




    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