{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T02:40:10Z","timestamp":1739414410632,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642104510"},{"type":"electronic","value":"9783642104527"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10452-7_12","type":"book-chapter","created":{"date-parts":[[2009,11,4]],"date-time":"2009-11-04T08:37:26Z","timestamp":1257323846000},"page":"170-185","source":"Crossref","is-referenced-by-count":0,"title":["Towards Safe Design of Synchronous Bus Protocols in Event-B"],"prefix":"10.1007","author":[{"given":"Ricardo Bedin","family":"Fran\u00e7a","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leandro Buss","family":"Becker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Paul","family":"Bodeveix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Marie","family":"Farines","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book: Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"12_CR2","unstructured":"AMBA Specification (Rev. 2). ARM Limited (1999)"},{"issue":"6","key":"12_CR3","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K. Apt","year":"1986","unstructured":"Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett.\u00a022(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"12_CR4","unstructured":"Ball, E., Butler, M.: Event-B patterns for specifying fault-tolerance in multi-agent interaction. In: Workshop on Methods, Models and Tools for Fault Tolerance, Oxford, pp. 4\u201313 (2007)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Berry, G., Kishinevsky, M., Singh, S.: System Level Design and Verification Using a Synchronous Language. In: ICCAD 2003: Proceedings of the 2003 IEEE\/ACM international conference on Computer-aided design, San Jose, p. 433 (2003)","DOI":"10.1109\/ICCAD.2003.159720"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-45648-1_2","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"D. Cansell","year":"2002","unstructured":"Cansell, D., Gopalakrishnan, G., Jones, M., M\u00e9ry, D., Weinzoepflen, A.: Incremental proof of the producer\/consumer property for the PCI Protocol. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 22\u201341. Springer, Heidelberg (2002)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/11955757_13","volume-title":"B 2007: Formal Specification and Development in B","author":"D. Cansell","year":"2006","unstructured":"Cansell, D., M\u00e9ry, D., Rehm, J.: Time constraint patterns for event B development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 140\u2013154. Springer, Heidelberg (2006)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-48153-2_14","volume-title":"Correct Hardware Design and Verification Methods","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Jha, S., Lu, Y., Wang, D.: Abstract BDDs: A technique for using abstraction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 172\u2013187. Springer, Heidelberg (1999)"},{"key":"12_CR9","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1145\/199448.199468","volume-title":"POPL 1995: Proceedings of the 22nd ACM SIGPLAN-SIGACT","author":"E. Emerson","year":"1995","unstructured":"Emerson, E., Namjoshi, K.: Reasoning about rings. In: POPL 1995: Proceedings of the 22nd ACM SIGPLAN-SIGACT, pp. 85\u201394. ACM, New York (1995)"},{"key":"12_CR10","unstructured":"Fran\u00e7a, R.B., Farines, J.-M., Bodeveix, J.-P., Becker, L.B., Filali, M.: Modeling a Bus Protocol: an Incremental Approach. In: 9th WTR. Bel\u00e9m (2007)"},{"key":"12_CR11","unstructured":"Fran\u00e7a, R.B.: An Approach for Modeling and Verification of Synchronous Bus Protocols (Uma Abordagem para Modelagem e Verifica\u00e7\u00e3o de Protocolos S\u00edncronos de Barramentos de Comunica\u00e7\u00e3o). Master\u2019s dissertation, SAID\/Universit\u00e9 de Toulouse (2008), UFSC, Florian\u00f3polis (2009), www.tede.ufsc.br\/teses\/PEAS0008-D.pdf"},{"key":"12_CR12","volume-title":"Workshop on Engineering Fault Tolerant Systems","author":"A. Lliasov","year":"2007","unstructured":"Lliasov, A.: Refinement patterns for rapid development of dependable systems. In: Workshop on Engineering Fault Tolerant Systems, article no. 10. ACM, Dubrovnik (2007)"},{"key":"12_CR13","unstructured":"Metayer, C., Abrial, J.-R., Voisin, L.: Rodin Deliverable D7: Event B language. Project IST-511599, School of Computing Science, University of Newcastle (2005)"},{"key":"12_CR14","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1109\/ISSOC.2004.1411185","volume-title":"Proceedings of the 2004 International Symposium on System-on-Chip (SOC 2004)","author":"K. Oumalou","year":"2004","unstructured":"Oumalou, K., Habibi, A., Tahar, S.: Design for Verification of a PCI Bus in System C. In: Proceedings of the 2004 International Symposium on System-on-Chip (SOC 2004), pp. 201\u2013204. IEEE, Tampere (2004)"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Pal, B., Banerjee, A., Dasgupta, P., Chakrabarti, P.: The BUSpec Platform for Automated Generation of Verification Aids for Standard Bus Protocols. In: MEMOCODE 2004, San Diego, pp. 119\u2013128 (2004)","DOI":"10.1109\/MEMCOD.2004.1459831"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/3-540-40922-X_21","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Shimizu","year":"2000","unstructured":"Shimizu, K., Dill, D., Hu, A.: Monitor-based formal specification of PCI. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 335\u2013353. Springer, Heidelberg (2000)"},{"key":"12_CR17","volume-title":"Computer Organization and Architecture - Designing for Performance","author":"W. Stallings","year":"1994","unstructured":"Stallings, W.: Computer Organization and Architecture - Designing for Performance. Prentice Hall, Englewood Cliffs (1994)"},{"key":"12_CR18","first-page":"181","volume-title":"Approches Formelles dans l\u2019Assistance au D\u00e9veloppement de Logiciels","author":"Y. Zimmermann","year":"2007","unstructured":"Zimmermann, Y.: D\u00e9veloppement formel de circuits \u00e9lectroniques par la m\u00e9thode B. In: Approches Formelles dans l\u2019Assistance au D\u00e9veloppement de Logiciels, pp. 181\u2013198. ACM, Namur (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10452-7_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T02:01:09Z","timestamp":1739412069000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10452-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642104510","9783642104527"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10452-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}