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 gatelevel.
Chapter PDF
Similar content being viewed by others
References
Berry, G., Kishinevsky, M., Singh, S.: System level design and verification using a synchronous language. In: ICCAD, pp. 433–440 (2003)
Bevier, W., Young, W.: The proof of correctness of a fault-tolerant circuit design. In: Second IFIP Conference on Dependable Computing For Critical Applications, pp. 107–114 (1991)
Beyer, S., Böhm, P., Gerke, M., Hillebrand, M., In der Rieden, T., Knapp, S., Leinenbach, D., Paul, W.J.: Towards the formal verification of lower system layers in automotive systems. In: ICCD ’05, pp. 317–324. IEEE Computer Society (2005)
Brown, G.M., Pike, L.: Easy parameterized verification of biphase mark and 8N1 protocols. In: TACAS’06, LNCS, vol. 3920, pp. 58–72. Springer (2006)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Marco Pistore, M.R., Sebastiani, R., Tacchella, A.: NuSMV 2: An open source tool for symbolic model checking. In: CAV ’02, pp. 359–364. Springer-Verlag (2002)
Ferdinand, C., Martin, F., Wilhelm, R., Alt, M.: Cache Behavior Prediction by Abstract Interpretation. Sci. Comput. Program. 35(2), 163–189 (1999)
Hillebrand, M., In der Rieden, T., Paul, W.: Dealing with I/O devices in the context of pervasive system verification. In: ICCD ’05, pp. 309–316. IEEE Computer Society (2005)
Knapp, S., Paul,W.: RealisticWorst Case Execution Time Analysis in the Context of Pervasive System Verification. In: Program Analysis and Compilation, LNCS, vol. 4444, pp. 53–81 (2007)
Lamport, L., Melliar-Smith, P.M.: Synchronizing clocks in the presence of faults. J. ACM 32(1), 52–78 (1985)
Miner, P.S., Johnson, S.D.: Verification of an optimized fault-tolerant clock synchronization circuit. In: Designing Correct Circuits. Springer (1996)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)
Pfeifer, H., Schwier, D., von Henke, F.W.: Formal verification for time-triggered clock synchronization. In: DCCA-7, vol. 12, pp. 207–226. IEEE Computer Society, San Jose, CA (1999)
Pike, L.: Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules. In: FMCAD’07, pp. 231–238 (2007)
Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Transactions on Software Engineering 25(5), 651–660 (1999)
Rushby, J.: An overview of formal verification for the time-triggered architecture. In: FTRTFT’02, LNCS, vol. 2469, pp. 83–105. Springer-Verlag, Oldenburg, Germany (2002)
Schmaltz, J.: A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware. In: FMCAD’07, pp. 223–230. IEEE/ACM, Austin, TX, USA (2007)
Shankar, N.: Mechanical verification of a generalized protocol for byzantine fault tolerant clock synchronization. In: FTRTFT’92, vol. 571, pp. 217–236. Springer, Netherlands (1992)
Tverdyshev, S., Alkassar, E.: Efficient bit-level model reductions for automated hardware verification. In: TIME 2008, to appear. IEEE Computer Society Press (2008)
Zhang, B.: On the Formal Verification of the FlexRay Communication Protocol. Automatic Verification of Critical Systems (AVoCS’06) pp. 184–189 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer Science+Business Media, LLC
About this paper
Cite this paper
Alkassar, E., Böhm, P., Knapp, S. (2008). Formal Correctness of an Automotive Bus Controller Implementation at Gate-Level. In: Kleinjohann, B., Wolf, W., Kleinjohann, L. (eds) Distributed Embedded Systems: Design, Middleware and Resources. DIPES 2008. IFIP – The International Federation for Information Processing, vol 271. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-09661-2_6
Download citation
DOI: https://doi.org/10.1007/978-0-387-09661-2_6
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-09660-5
Online ISBN: 978-0-387-09661-2
eBook Packages: Computer ScienceComputer Science (R0)