Formal Correctness of an Automotive Bus Controller Implementation at Gate-Lavel
Eyad Alkassar, Peter Böhm and Steffen Knapp abstract
We formalize the correctness of a real-time scheduler in a time-triggered architecture. Where previous research elaborated on real-time protocol correctness, we extend this work to gate-level hardware. This requires a sophisticated analysis of analog bit-level synchronization and message transmission. Our case-study is a concrete automotive bus controller (ABC). For a set of interconnected ABCs we 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 our knowledge, this is the first effort formally tackling scheduler correctness at gate-level.
infobook title | Distributed Embedded Systems: Design, Middleware and Resources - IFIP 20th World Computer Congress, TC 10 Working Conference on Distributed and Parallel Embedded Systems (DIPES'08) |
editor | Kleinjohann, Bernd and Kleinjohann, Lisa and Wolf, Wayne |
pages | 57—67 |
publisher | Springer Science and Business Media |
volume | 271/2008 |
year | 2008 |
links
BibTeX
DOI (10.1007/978-0-387-09661-2_6)
related pages
|
