{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:29:56Z","timestamp":1755217796843,"version":"3.43.0"},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"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":[[2003,3]]},"DOI":"10.1023\/a:1022965204416","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T18:16:51Z","timestamp":1049739411000},"page":"109-116","source":"Crossref","is-referenced-by-count":4,"title":["Experience with Applying Formal Methods to Protocol Specification and System Architecture"],"prefix":"10.1007","volume":"22","author":[{"given":"Mani","family":"Azimi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ching-Tsun","family":"Chou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akhilesh","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor W.","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phamndra K.","family":"Mannava","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Seungjoon","family":"Park","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"PCI ExpressTM web site: www.pcisig.com\/specifications\/pci_express.","key":"5117026_CR1"},{"issue":"2","key":"5117026_CR2","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1109\/MM.2002.997878","volume":"22","author":"F. Briggs","year":"2002","unstructured":"F. Briggs, M. Cekleov, K. Creta, M. Khare, S. Kulick, A. Kumar, L.P. Looi, C. Natarajan, S. Radhakrishnan, and L. Rankin, \u201cIntel 870: A building block for cost-effective, scalable servers,\u201d IEEE Micro, Vol. 22, No. 2, pp. 36\u201347, 2002.","journal-title":"IEEE Micro"},{"issue":"8","key":"5117026_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, \u201cGraph-based algorithms for Boolean function manipulation,\u201d IEEE Trans. on Computers, Vol. C-35, No. 8, pp. 677\u2013691, 1986.","journal-title":"IEEE Trans. on Computers"},{"doi-asserted-by":"crossref","unstructured":"F. Corella, R. Shaw, and C. Zhang, \u201cA formal proof of absence of deadlock for any acyclic network of PCI buse,\u201d Hardware Description Languages and Their Applications, Chapman & Hall, pp. 134\u2013156, 1997.","key":"5117026_CR4","DOI":"10.1007\/978-0-387-35064-6_15"},{"doi-asserted-by":"crossref","unstructured":"W.J. Dally and C.L. Seitz, \u201cDeadlock-free message routing in multiprocessor interconnection networks,\u201d IEEE Trans. on Computers, Vol. C-36, No. 5, 1987.","key":"5117026_CR5","DOI":"10.1109\/TC.1987.1676939"},{"unstructured":"M. Haycock and R. Mooney, \u201cA 2.5GB\/s bidirectional signaling technology,\u201d Hot Interconnects V, pp. 149\u2013156, 1997.","key":"5117026_CR6"},{"issue":"4","key":"5117026_CR7","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1109\/54.936245","volume":"18","author":"R.B. Jones","year":"2001","unstructured":"R.B. Jones, J.W. O'Leary, C.-J.H. Seger, M.D. Aagaard, and T.F. Melham, \u201cPractical formal verification in microprocessor design,\u201d IEEE Design and Test of Computers, Vol. 18, No. 4, pp. 16\u201325, 2001.","journal-title":"IEEE Design and Test of Computers"},{"doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.","key":"5117026_CR8","DOI":"10.1007\/978-1-4615-3190-6"},{"doi-asserted-by":"crossref","unstructured":"K.L. McMillan, \u201cA compositional rule for hardware design refinement,\u201d Computer Aided Verification (CAV'97), in O. Grumberg (Ed.), LNCS 1254, pp. 24\u201335, 1997.","key":"5117026_CR9","DOI":"10.1007\/3-540-63166-6_6"},{"issue":"2","key":"5117026_CR10","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1109\/2.191995","volume":"26","author":"L.M. Ni","year":"1993","unstructured":"L.M. Ni and P.K. McKinley, \u201cA survey of wormhole routing techniques in direct networks,\u201d IEEE Computer Magazine, Vol. 26, No. 2, pp. 62\u201376, 1993.","journal-title":"IEEE Computer Magazine"},{"issue":"2","key":"5117026_CR11","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"C.-J.H. Seger and R.E. Bryant, \u201cFormal verification by symbolic evaluation of partially ordered trajectories,\u201d Formal Methods in System Design, Vol. 6, No. 2, pp. 147\u2013190, 1995.","journal-title":"Formal Methods in System Design"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022965204416.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1022965204416\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022965204416.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:23:20Z","timestamp":1754421800000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1022965204416"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":11,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["5117026"],"URL":"https:\/\/doi.org\/10.1023\/a:1022965204416","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}