Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method

Joris Rehm 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a model of the IEEE 1394 Root Contention Protocol with a proof of Safety. This model has real-time properties which are expressed in the language of the event B method: first-order classical logic and set theory. Verification is done by proof using the event B method and its prover, we also have a way to model-check models. Refinement is used to describe the studied system at different levels of abstraction: first without time to fix the scheduling of events abstracly, and then with more and more time constraints.
Type de document :
Article dans une revue
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2010, Special Section On ISOLA 2007, 12 (1), pp.39-51. 〈10.1007/s10009-009-0130-5〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00336624
Contributeur : Joris Rehm <>
Soumis le : mardi 4 novembre 2008 - 15:59:50
Dernière modification le : mardi 24 avril 2018 - 13:51:25
Document(s) archivé(s) le : mardi 9 octobre 2012 - 15:00:44

Fichier

rcp_sttt.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Joris Rehm. Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2010, Special Section On ISOLA 2007, 12 (1), pp.39-51. 〈10.1007/s10009-009-0130-5〉. 〈inria-00336624〉

Partager

Métriques

Consultations de la notice

198

Téléchargements de fichiers

100