Formal Correctness of an Automotive Bus Controller Implementation at Gate−Lavel
Eyad Alkassar‚ Peter B"ohm 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.
Details
| Book 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
DOI (10.1007/978-0-387-09661-2_6)
Related pages
|
People |