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 [13],[15], the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts.
Supported in part by NSF grants CCR-9987516 and CCR-00814006 and in part by NSF/CNRS cooperation project 1998-2000 and PRST IL/QSL/DIXIT project
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
P. A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling global conditions in parameterized system verification. In Nicolas Halbwachs and Doron Peled, editors, Computer-Aided Verification, CAV’ 99, volume 1633 of Lecture Notes in Computer Science, pages 134–145, Trento, Italy, July 1999. Springer-Verlag.
J.-R. Abrial. Extending b without changing it (for developing distributed systems). In H. Habrias, editor, 1st Conference on the B method, pages 169–190, November 1996.
J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In D. Bert, editor, B’98: Recent Advances in the Development and Use of the B Method, volume 1393 of Lecture Notes in Computer Science. Springer-Verlag, 1998.
Jean-Raymond Abrial. The B Book-Assigning Programs to Meanings. Cambridge University Press, 1996.
R. J. R. Back. On correct refinement of programs. Journal of Computer and System Sciences, 23(1):49–68, 1979.
R. J. R. Back and K. Sere. Stepwise refinement of action systems. In J. L. A van de Snepscheut, editor, Mathematics for ProgramConstruction, pages 113–138. Springer-Verlag, june 1989. LNCS 375.
Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter. Routing information protocol in HOL/SPIN. In Theorem Provers in Higher-Order Logics 2000: TPHOLs00, August 2000.
M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many identical finite state processes. Information and Computation, 81:13–31, April 1989.
K. M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0-201-05866-9.
Edmund Clarke, Somesh Jha, Yuan Lu, and Dong Wang. Abstract BDDs: A technique for using abstraction in model checking. In Laurence Pierre and Thomas Kropf, editors, Correct Hardware Design and Verification Methods, CHARME’ 99, volume 1703 of Lecture Notes in Computer Science, Bad Herrenalb, Germany, September 1999. Springer-Verlag.
Francisco Corella. Proposal to fix ordering problem in PCI 2.1, 1996. Accessed June 2001 http://www.pcisig.com/reflector/thrd8.html#00704.
F. K. Hwang, D. S. Richards, and P. Winter. The Steiner Tree Problem, volume 53 of Annals of Discrete Mathematics. North-Holland, Amsterdam, Netherlands, 1992.
Michael Jones and Ganesh Gopalakrishnan. Verifying transaction ordering properties in unbounded bus networks through combined deductive/algorithmic methods. InWarren A. Hunt Jr. and Steven D. Johnson, editors, Formal Methods in Computer-Aided Design: FMCAD’00, number 1954 in LNCS, page 505, Austin, Texas, November 2000.
Y. Kesten, O. Maler, M. Marcus, A Pnueli, and E. Shahar. symbolic model checking with rich assertional languages. In Orna Grumburg, editor, Computer-Aided Verification, CAV’ 97, volume 1254 of Lecture Notes in Computer Science, Haifa, Israel, June 1997. Springer-Verlag.
Abdel Mokkedem, Ravi Hosabettu, Michael D. Jones, and Ganesh Gopalakrishnan. Formalization and proof of a solution to the PCI 2.1 bus transaction ordering problem. Formal Methods in Systems Design, 16(1):93–119, January 2000.
PCISIG. PCI Special Interest Group-PCI Local Bus Specification, Revision 2.1, June 1995.
Amir Pnueli and Elad Shahar. Liveness and acceleration in parameterized verification. In E. Allen Emerson and A. Prasad Sistla, editors, Computer-Aided Verification, CAV’ 00, volume 1855 of Lecture Notes in Computer Science, pages 328–343, Chicago, IL, July 2000. Springer-Verlag.
A. Roychoudhurry, K. N. Kumar, C. R. Ramakrishnan, I.V. Ramakrishnan, and S. A. Smolka. Verification of parameterized systems using logic program transformations. In S. Graf and M. Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1785 of Lecture Notes in Computer Science, pages 172–187. Springer-Verlag, 2000.
Kanna Shimizu, David L. Dill, and Alan J. Hu. Monitor-based formal specification of PCI. In Warran A. Hunt Jr. and Steven D. Johnson, editors, Formal Methods in Computer-Aided Design: FMCAD’00, number 1954 in LNCS, page 335, Austin, Texas, November 2000.
STERIA-Technologies de l’Information,Aix-en-Provence (F). Atelier B, Manuel Utilisateur, 3.5 edition, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cansell, D., Gopalakrishnan, G., Jones, M., Méry, D., Weinzoepflen, A. (2002). Incremental Proof of the Producer/Consumer Property for the PCI Protocol. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds) ZB 2002:Formal Specification and Development in Z and B. ZB 2002. Lecture Notes in Computer Science, vol 2272. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45648-1_2
Download citation
DOI: https://doi.org/10.1007/3-540-45648-1_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43166-4
Online ISBN: 978-3-540-45648-3
eBook Packages: Springer Book Archive