{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:16:54Z","timestamp":1725484614912},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540431664"},{"type":"electronic","value":"9783540456483"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45648-1_2","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T01:26:02Z","timestamp":1180315562000},"page":"22-41","source":"Crossref","is-referenced-by-count":9,"title":["Incremental Proof of the Producer\/Consumer Property for the PCI Protocol"],"prefix":"10.1007","author":[{"given":"Dominique","family":"Cansell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mike","family":"Jones","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"M\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Airy","family":"Weinzoepflen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,1,22]]},"reference":[{"key":"2_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"Computer-Aided Verification, CAV\u2019 99","author":"P. A. Abdulla","year":"1999","unstructured":"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\u2019 99, volume 1633 of Lecture Notes in Computer Science, pages 134\u2013145, Trento, Italy, July 1999. Springer-Verlag."},{"key":"2_CR2","unstructured":"J.-R. Abrial. Extending b without changing it (for developing distributed systems). In H. Habrias, editor, 1st Conference on the B method, pages 169\u2013190, November 1996."},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"J.-R. Abrial","year":"1998","unstructured":"J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In D. Bert, editor, B\u201998: Recent Advances in the Development and Use of the B Method, volume 1393 of Lecture Notes in Computer Science. Springer-Verlag, 1998."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Jean-Raymond Abrial. The B Book-Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"issue":"1","key":"2_CR5","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","volume":"23","author":"R. J. R. Back","year":"1979","unstructured":"R. J. R. Back. On correct refinement of programs. Journal of Computer and System Sciences, 23(1):49\u201368, 1979.","journal-title":"Journal of Computer and System Sciences"},{"key":"2_CR6","series-title":"Lect Notes Comput Sci","first-page":"113","volume-title":"Mathematics for ProgramConstruction","author":"R. J. R. Back","year":"1989","unstructured":"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\u2013138. Springer-Verlag, june 1989. LNCS 375."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/3-540-44659-1_4"},{"key":"2_CR8","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M.C. Browne","year":"1989","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many identical finite state processes. Information and Computation, 81:13\u201331, April 1989.","journal-title":"Information and Computation"},{"key":"2_CR9","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0-201-05866-9."},{"key":"2_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Correct Hardware Design and Verification Methods, CHARME\u2019 99","author":"E. Clarke","year":"1999","unstructured":"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\u2019 99, volume 1703 of Lecture Notes in Computer Science, Bad Herrenalb, Germany, September 1999. Springer-Verlag."},{"key":"2_CR11","unstructured":"Francisco Corella. Proposal to fix ordering problem in PCI 2.1, 1996. Accessed June 2001 http:\/\/www.pcisig.com\/reflector\/thrd8.html#00704 ."},{"key":"2_CR12","unstructured":"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."},{"key":"2_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/3-540-40922-X_31","volume-title":"Formal Methods in Computer-Aided Design: FMCAD\u201900","author":"M. Jones","year":"2000","unstructured":"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\u201900, number 1954 in LNCS, page 505, Austin, Texas, November 2000."},{"key":"2_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification, CAV\u2019 97","author":"Y. Kesten","year":"1997","unstructured":"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\u2019 97, volume 1254 of Lecture Notes in Computer Science, Haifa, Israel, June 1997. Springer-Verlag."},{"issue":"1","key":"2_CR15","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1023\/A:1008729625855","volume":"16","author":"A. Mokkedem","year":"2000","unstructured":"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\u2013119, January 2000.","journal-title":"Formal Methods in Systems Design"},{"key":"2_CR16","unstructured":"PCISIG. PCI Special Interest Group-PCI Local Bus Specification, Revision 2.1, June 1995."},{"key":"2_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/10722167_26","volume-title":"Computer-Aided Verification, CAV\u2019 00","author":"A. Pnueli","year":"2000","unstructured":"Amir Pnueli and Elad Shahar. Liveness and acceleration in parameterized verification. In E. Allen Emerson and A. Prasad Sistla, editors, Computer-Aided Verification, CAV\u2019 00, volume 1855 of Lecture Notes in Computer Science, pages 328\u2013343, Chicago, IL, July 2000. Springer-Verlag."},{"key":"2_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-46419-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Roychoudhurry","year":"2000","unstructured":"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\u2013187. Springer-Verlag, 2000."},{"key":"2_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/3-540-40922-X_21","volume-title":"Formal Methods in Computer-Aided Design: FMCAD\u201900","author":"K. Shimizu","year":"2000","unstructured":"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\u201900, number 1954 in LNCS, page 335, Austin, Texas, November 2000."},{"key":"2_CR20","unstructured":"STERIA-Technologies de l\u2019Information,Aix-en-Provence (F). Atelier B, Manuel Utilisateur, 3.5 edition, 1998."}],"container-title":["Lecture Notes in Computer Science","ZB 2002:Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45648-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T07:14:31Z","timestamp":1556435671000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45648-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540431664","9783540456483"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45648-1_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}