Incremental Proof of the Producer/Consumer Property for the PCI Protocol
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 ,, the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts.
KeywordsModel Check Steiner Tree Steiner Point Proof Obligation Abstract System
Unable to display preview. Download preview PDF.
- 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.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.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.Jean-Raymond Abrial. The B Book-Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
- 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.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.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.K. M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0-201-05866-9.Google Scholar
- 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.Francisco Corella. Proposal to fix ordering problem in PCI 2.1, 1996. Accessed June 2001 http://www.pcisig.com/reflector/thrd8.html#00704.
- 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.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.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
- 16.PCISIG. PCI Special Interest Group-PCI Local Bus Specification, Revision 2.1, June 1995.Google Scholar
- 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.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
- 20.STERIA-Technologies de l’Information,Aix-en-Provence (F). Atelier B, Manuel Utilisateur, 3.5 edition, 1998.Google Scholar