Incremental Proof of the Producer/Consumer Property for the PCI Protocol

Abstract : We present an incremental proof of the producer/consumer property for the PCI protocol. In the incremental proof, a corrected model of the multi-bus PCI 2.1 protocol is shown to be a refinement of the producer/consumer property. Multi-bus PCI must be corrected because the original PCI specification violates the producer/consumer property. The final model of PCI includes transaction types and reordering along with the completion mechanism for delayed PCI transactions. Verification results include multiple concurrent sessions of the producer/consumer property in a family of topologically isomorphic network configurations. The remaining configurations are identified and left for future work. In contrast to previous case studies involving this problem~\cite{jones:fmcad00,mokkedem:fmsd00}, the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts.
Type de document :
Communication dans un congrès
D. Bert, J.P. Bowen, M.C. Henson, K. Robinson. 2nd International Conference of B and Z Users - ZB 2002, 2002, Grenoble, France, Springer, 2272, pp.22-41, 2002, Lectures Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00100888
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:52:42
Dernière modification le : mardi 24 avril 2018 - 13:32:47

Identifiants

  • HAL Id : inria-00100888, version 1

Collections

Citation

Dominique Cansell, Ganesh Gopalakrishnan, Mike Jones, Dominique Méry, Airy Weinzoepflen. Incremental Proof of the Producer/Consumer Property for the PCI Protocol. D. Bert, J.P. Bowen, M.C. Henson, K. Robinson. 2nd International Conference of B and Z Users - ZB 2002, 2002, Grenoble, France, Springer, 2272, pp.22-41, 2002, Lectures Notes in Computer Science. 〈inria-00100888〉

Partager

Métriques

Consultations de la notice

148