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.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.184-189, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00091667
Contributeur : Stephan Merz <>
Soumis le : mercredi 6 septembre 2006 - 19:32:42
Dernière modification le : mercredi 6 septembre 2006 - 20:46:00
Document(s) archivé(s) le : jeudi 20 septembre 2012 - 10:23:12

Fichier

Identifiants

  • HAL Id : inria-00091667, version 1

Collections

Citation

Bo Zhang. On the Formal Verification of the FlexRay Communication Protocol. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.184-189, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00091667〉

Partager

Métriques

Consultations de la notice

126

Téléchargements de fichiers

191