Skip to Main content Skip to Navigation
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 metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/inria-00091667
Contributor : Stephan Merz <>
Submitted on : Wednesday, September 6, 2006 - 7:32:42 PM
Last modification on : Wednesday, September 6, 2006 - 8:46:00 PM
Long-term archiving on: : Thursday, September 20, 2012 - 10:23:12 AM

Identifiers

  • HAL Id : inria-00091667, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

170

Files downloads

293