Skip to Main content Skip to Navigation
New interface
Conference papers

On the Formal Verification of the FlexRay Communication Protocol

Abstract : We present ongoing work on the formal analysis of the FlexRay communication protocol. Isabelle/HOL, a theorem prover for Higher Order Logic, is chosen as our specification and verification system. Essential properties of the FlexRay protocol are identified, formalized and verified. In particular, we show our formal verification of the FlexRay bus guardian component. Furthermore, some insights for the formal verification of the clock synchronization algorithm are exposed.
Document type :
Conference papers
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Wednesday, September 6, 2006 - 7:32:42 PM
Last modification on : Thursday, January 6, 2022 - 11:38:04 AM
Long-term archiving on: : Thursday, September 20, 2012 - 10:23:12 AM


  • HAL Id : inria-00091667, version 1



Bo Zhang. On the Formal Verification of the FlexRay Communication Protocol. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.184-189. ⟨inria-00091667⟩



Record views


Files downloads