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

  • Dominique Cansell
  • Ganesh Gopalakrishnan
  • Mike Jones
  • Dominique Méry
  • Airy Weinzoepflen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


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.


Model Check Steiner Tree Steiner Point Proof Obligation Abstract System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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.CrossRefGoogle Scholar
  2. 2.
    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.Google Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    Jean-Raymond Abrial. The B Book-Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
  5. 5.
    R. J. R. Back. On correct refinement of programs. Journal of Computer and System Sciences, 23(1):49–68, 1979.CrossRefMathSciNetGoogle Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    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.Google Scholar
  8. 8.
    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.Google Scholar
  9. 9.
    K. M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0-201-05866-9.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    Francisco Corella. Proposal to fix ordering problem in PCI 2.1, 1996. Accessed June 2001
  12. 12.
    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.Google Scholar
  13. 13.
    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.CrossRefGoogle Scholar
  14. 14.
    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.Google Scholar
  15. 15.
    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.CrossRefGoogle Scholar
  16. 16.
    PCISIG. PCI Special Interest Group-PCI Local Bus Specification, Revision 2.1, June 1995.Google Scholar
  17. 17.
    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.CrossRefGoogle Scholar
  18. 18.
    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.CrossRefGoogle Scholar
  19. 19.
    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.CrossRefGoogle Scholar
  20. 20.
    STERIA-Technologies de l’Information,Aix-en-Provence (F). Atelier B, Manuel Utilisateur, 3.5 edition, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Dominique Cansell
    • 1
  • Ganesh Gopalakrishnan
    • 2
  • Mike Jones
    • 3
  • Dominique Méry
    • 1
  • Airy Weinzoepflen
    • 1
  1. 1.LORIANancyFrance
  2. 2.University of UtahSalt Lake CityUSA
  3. 3.presently at Brigham Young UniversityProvoUSA

Personalised recommendations