{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:17:08Z","timestamp":1755217028239,"version":"3.43.0"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2000,1]]},"DOI":"10.1023\/a:1008729625855","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"93-119","source":"Crossref","is-referenced-by-count":12,"title":["Formalization and Analysis of a Solution to the PCI 2.1 Bus Transaction Ordering Problem"],"prefix":"10.1007","volume":"16","author":[{"given":"Abdel","family":"Mokkedem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ravi M.","family":"Hosabettu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael D.","family":"Jones","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ganesh C.","family":"Gopalakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"243848_CR1","unstructured":"R.W. Butler and J.A. Sjogren, \u201cA PVS graph theory library,\u201d Technical Report Memorandum, NASA Langly Research Center. http:\/\/atb-www.larc.nasa.gov\/ftp\/larc\/PVS-library, 1997."},{"key":"243848_CR2","unstructured":"E.M. Clarke, O. Grumberg, H. Haraishi, S. Jha, D. Long, K.L. McMillan, and L. Ness, \u201cVerification of the futurebus+ cache coherence protocol,\u201d Technical Report CMU-CS-92-206, School of Computer Science, Carnegie Mellon University, 1992."},{"key":"243848_CR3","unstructured":"F. Corella, \u201cProposal to fix ordering problem in PCI 2.1,\u201d http:\/\/www.pcisig.com\/reflector\/thrd8.htm1#00706. 1996."},{"key":"243848_CR4","unstructured":"F. Corella, \u201cVerifying memory ordering model of I\/O system,\u201d in '97, Toledo, Spain, 1997. Invited Talk."},{"key":"243848_CR5","doi-asserted-by":"crossref","unstructured":"F. Corella, R. Shaw, and C. Zhang, \u201cA formal proof of absence of dead-lock for any acyclic network of PCI buses,\u201d in '97. Toledo, Spain, 1997.","DOI":"10.1007\/978-0-387-35064-6_15"},{"key":"243848_CR6","doi-asserted-by":"crossref","unstructured":"R. Ghughal, A. Mokkedem, R. Nalumasu, and G. Gopalakrishnan, \u201cUsing \u2018test model-checking\u2019 to verify the runway-PA8000 memory model,\u201d in Tenth ACM Symposium on Parallel Algorithms and Architectures. Puerto Vallarta, Mexico, 1998, pp. 231\u2013239.","DOI":"10.1145\/277651.277689"},{"key":"243848_CR7","doi-asserted-by":"crossref","unstructured":"G. Gopalakrishnan, R. Ghughal, R. Hosabettu, A. Mokkedem, and R. Nalumasu, \u201cFormal modeling and validation applied to a commercial coherent bus: A case study,\u201d in H.F. Li and D.K. Probst (Eds.), '97. Montreal, Canada, 1997, pp. 48\u201362.","DOI":"10.1007\/978-0-387-35190-2_4"},{"key":"243848_CR8","unstructured":"G. Holzmann, Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"243848_CR9","doi-asserted-by":"crossref","unstructured":"A. Mokkedem, R.M. Hosabettu, M.D. Jones, and G. Gopalakrishnan, \u201cFormalization and analysis of a solution to the PCI 2.1 bus transaction ordering problem: PVS files,\u201d Technical Report UUCS-99-007, 1999.","DOI":"10.1007\/3-540-49519-3_17"},{"key":"243848_CR10","unstructured":"V. Nagasamy, S. Rajan, and P.R. Panda, \u201cFiber channel protocol: Formal specification and verification,\u201d in Sixth Annual Silicon Valley Networking Conference, 1997."},{"key":"243848_CR11","first-page":"464","volume":"1427","author":"R. Nalumasu","year":"1998","unstructured":"R. Nalumasu, R. Ghughal, A. Mokkedem, and G. Gopalakrishnan, \u201cThe \u2018test model-checking\u2019 approach to the verification of formal memory models of multiprocessors,\u201d in Lecture Notes in Computer Science, Vol. 1427 of Lecture Notes in Computer Science. Vancouver, BC, Canada, 1998, pp. 464\u2013476.","journal-title":"The \u2018test model-checking\u2019 approach to the verification of formal memory models of multiprocessors"},{"issue":"2","key":"243848_CR12","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke, \u201cFormal verification for fault-tolerant architectures: Prolegomena to the design of PVS,\u201d IEEE Transactions on Software Engineering Vol. 21, No. 2, pp. 107\u2013125, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"243848_CR13","series-title":"Lecture Notes in Compuer Science","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/3-540-61474-5_78","volume-title":"'96","author":"S. Park","year":"1996","unstructured":"S. Park and D.L. Dill, \u201cProtocol verification by aggregation of distributed action,\u201d in R. Alur and T.A. Henzinger (Eds.), '96, Vol. 1102 of Lecture Notes in Compuer Science. New Brunswick, NJ, 1996, pp. 300\u2013310."},{"key":"243848_CR14","unstructured":"PCISIG, \u2018PCI Special Interest Group\u2013PCI Local Bus Specification, Revision 2.1', 1995."},{"key":"243848_CR15","unstructured":"E. Solari and G. Willse, PCI Hardware and Software Architecture & Design. Annabooks, 3rd edition, ISBN 0-929392-32-9, 1996."},{"key":"243848_CR16","unstructured":"VSI Alliance, \u201cInterface standards for design re-use of virtual components,\u201d http:\/\/www.vsi.org\/."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008729625855.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008729625855\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008729625855.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:24:56Z","timestamp":1754367896000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008729625855"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,1]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,1]]}},"alternative-id":["243848"],"URL":"https:\/\/doi.org\/10.1023\/a:1008729625855","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2000,1]]}}}