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.
Formal correctness of an automotive bus controller implementation at gate-level
Formale Richtigkeit einer Kraftfahrzeug-Buscontroller-Implementierung auf Gatterebene
2008
11 Seiten, 3 Bilder, 19 Quellen
Conference paper
English
Timing Correctness in Safety-Related Automotive Software
SAE Technical Papers | 2011
|Timing Correctness in Safety-Related Automotive Software
British Library Conference Proceedings | 2011
|Formal Analysis of the Structural Correctness of SLC Descriptions
British Library Online Contents | 2003
|European Patent Office | 2021