{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T01:10:04Z","timestamp":1744074604651,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642340611"},{"type":"electronic","value":"9783642340628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34062-8_28","type":"book-chapter","created":{"date-parts":[[2012,9,7]],"date-time":"2012-09-07T08:52:58Z","timestamp":1347007978000},"page":"211-220","source":"Crossref","is-referenced-by-count":2,"title":["Formal Modeling and Model Checking Analysis of the Wishbone System-on-Chip Bus Protocol"],"prefix":"10.1007","author":[{"given":"Ricai","family":"Luo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hua","family":"Tan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"ARM. Advanced microcontroller bus architecture specification [S\/OL] (1999), http:\/\/www.arm.com\/armtech\/AMBA_spec"},{"key":"28_CR2","unstructured":"IBM. 32-bit processor local bus architecture specifications [S\/OL], Version 2.9., http:\/\/www.ibm.com\/chips\/products\/coreconnect\/"},{"key":"28_CR3","unstructured":"Open-Core Protocol Int. Partnership Association Inc. Open-core protocol specification [S\/OL], Release 1.0 (2001), http:\/\/www.ocpip.org"},{"key":"28_CR4","unstructured":"WISHBONE, Revision B.3 Specification [S\/OL], http:\/\/www.opencores.org\/-projects.cgi\/web\/wishbone\/wishbone"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Roychoudhury, A., Mitra, T., Karri, S.R.: Using Formal Techniques to Debug the AMBA System-on-Chip Bus Protocol. In: The Design, Automation, and Test Europe Conference, Munich, Germany, pp. 828\u2013833 (March 2003)","DOI":"10.1109\/DATE.2003.1253709"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Chauhan, P., Clarke, E.M., Lu, Y., Wang, D.: Verifying IP-Core based System-On-Chip Designs. In: The IEEE International AS IC\/SOC Conference, pp. 27\u201331 (September 1999)","DOI":"10.1109\/ASIC.1999.806467"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Goel, A., Lee, W.R.: Formal verification of an IBM CoreConnect processor local bus arbiter core. In: DAC 2000, pp. 196\u2013200 (2000)","DOI":"10.1145\/337292.337384"},{"key":"28_CR8","unstructured":"Lin, H.-M., Yen, C.-C., Shih, C.-H., Jou, J.-Y.: On compliance test of on-chip bus for SOC. In: ASP-DAC 2004, pp. 328\u2013333 (2004)"},{"issue":"2","key":"28_CR9","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"28_CR10","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Carnegie-Mellon University publication CMU-CS-92-131 (May 1992)"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"28_CR12","unstructured":"Cadence Berkeley Laboratories, California, USA. The SMV Model Checker (1999), http:\/\/www-cad.eecs.berkeley.edu\/kenmcmil\/smv\/"}],"container-title":["Lecture Notes in Computer Science","Information Computing and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34062-8_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T00:30:38Z","timestamp":1744072238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34062-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642340611","9783642340628"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34062-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}