{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T15:37:06Z","timestamp":1725896226366},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642307287"},{"type":"electronic","value":"9783642307294"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30729-4_16","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T04:49:46Z","timestamp":1340772586000},"page":"221-236","source":"Crossref","is-referenced-by-count":5,"title":["Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems"],"prefix":"10.1007","author":[{"given":"Denisa","family":"Diaconescu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ioana","family":"Leustean","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigia","family":"Petre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kaisa","family":"Sere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gheorghe","family":"Stefanescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Design. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"6","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: An Open Toolset for Modelling and Reasoning in Event-B. International Journal on Software Tools for Technology Transfer\u00a06, 447\u2013466 (2010)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Back, R.J., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: Proceedings of the 2nd ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 131\u2013142 (1983)","DOI":"10.1145\/800221.806716"},{"key":"16_CR5","unstructured":"Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier (2001)"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"850","DOI":"10.1145\/268999.269004","volume":"44","author":"M. Broy","year":"1997","unstructured":"Broy, M.: Compositional refinement of interactive systems. Journal of the ACM\u00a044, 850\u2013891 (1997)","journal-title":"Journal of the ACM"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0304-3975(99)00322-9","volume":"258","author":"M. Broy","year":"2001","unstructured":"Broy, M., Stefanescu, G.: The algebra of stream processing functions. Theoretical Computer Science\u00a0258, 99\u2013129 (2001)","journal-title":"Theoretical Computer Science"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-15898-8_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"J. Bryans","year":"2010","unstructured":"Bryans, J., Wei, W.: Formal Analysis of BPMN Models Using Event-B. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol.\u00a06371, pp. 33\u201349. Springer, Heidelberg (2010)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-00255-7_2","volume-title":"Integrated Formal Methods","author":"M. Butler","year":"2009","unstructured":"Butler, M.: Decomposition Structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol.\u00a05423, pp. 20\u201338. Springer, Heidelberg (2009)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Diaconescu, D., Leustean, I., Petre, L., Sere, K., Stefanescu, G.: Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems. TUCS Technical Reports No. 1028 (December 2011), \n                  \n                    http:\/\/tucs.fi","DOI":"10.1007\/978-3-642-30729-4_16"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Dragoi, C., Stefanescu, G.: AGAPIA v0.1: A programming language for interactive systems and its typing systems. In: Proc. FINCO\/ETAPS 2007. ENTCS, vol.\u00a0203, pp. 69\u201394. Elsevier (2008)","DOI":"10.1016\/j.entcs.2008.04.087"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-540-77566-9_22","volume-title":"SOFSEM 2008: Theory and Practice of Computer Science","author":"C. Dragoi","year":"2008","unstructured":"Dragoi, C., Stefanescu, G.: On Compiling Structured Interactive Programs with Registers and Voices. In: Geffert, V., Karhum\u00e4ki, J., Bertoni, A., Preneel, B., N\u00e1vrat, P., Bielikov\u00e1, M. (eds.) SOFSEM 2008. LNCS, vol.\u00a04910, pp. 259\u2013270. Springer, Heidelberg (2008)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-20398-5_24","volume-title":"NASA Formal Methods","author":"A. Salehi Fathabadi","year":"2011","unstructured":"Salehi Fathabadi, A., Rezazadeh, A., Butler, M.: Applying Atomicity and Model Decomposition to a Space Craft System in Event-B. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 328\u2013342. Springer, Heidelberg (2011)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Hoang, T.S., F\u00fcrst, A., Abrial, J.-R.: Event-B Patterns and Their Tool Support. In: Proc. SEFM 2009, pp. 210\u2013219. IEEE (2009)","DOI":"10.1109\/SEFM.2009.17"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-17071-3_4","volume-title":"Formal Methods for Components and Objects","author":"A. Iliasov","year":"2010","unstructured":"Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A.: Patterns for Refinement Automation. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol.\u00a06286, pp. 70\u201388. Springer, Heidelberg (2010)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-11811-1_14","volume-title":"Abstract State Machines, Alloy, B and Z","author":"A. Iliasov","year":"2010","unstructured":"Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ilic, D., Latvala, T.: Supporting Reuse in Event B Development: Modularisation Approach. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 174\u2013188. Springer, Heidelberg (2010)"},{"key":"16_CR17","series-title":"LNCS","first-page":"236","volume-title":"FSEN 2011","author":"M. Kamali","year":"2011","unstructured":"Kamali, M., Petre, L., Sere, K., Daneshtalab, M.: Refinement-Based Modeling of 3D NoCs. In: Sirjani, M. (ed.) FSEN 2011. LNCS, vol.\u00a07141, pp. 236\u2013252. Springer, Heidelberg (2011)"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Kamali, M., Petre, L., Sere, K., Daneshtalab, M.: Formal Modeling of Multicast Communication in 3D NoCs. In: Proc. DSD 2011, pp. 634\u2013642. IEEE (2011)","DOI":"10.1109\/DSD.2011.86"},{"key":"16_CR19","unstructured":"Milner, R.: Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press (1999)"},{"issue":"1","key":"16_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes I and II. Information and Computation\u00a0100(1), 1\u201377 (1992)","journal-title":"Information and Computation"},{"key":"16_CR21","first-page":"1722","volume":"13","author":"A. Popa","year":"2007","unstructured":"Popa, A., Sofronia, A., Stefanescu, G.: High-level structured interactive programs with registers and voices. JUCS\u00a013, 1722\u20131754 (2007)","journal-title":"JUCS"},{"key":"16_CR22","first-page":"69","volume":"280","author":"S. Schneider","year":"2011","unstructured":"Schneider, S., Treharne, H., Wehrheim, H.: Bounded Retransmission in Event-B||CSP: a Case Study. ENTSC\u00a0280, 69\u201380 (2011)","journal-title":"ENTSC"},{"key":"16_CR23","first-page":"265","volume":"12","author":"A. Sofronia","year":"2009","unstructured":"Sofronia, A., Popa, A., Stefanescu, G.: Undecidability Results for Finite Interactive Systems. ROMJIST\u00a012, 265\u2013279 (2009); Also: Arxiv, CoRR 1001.0143 (2010)","journal-title":"ROMJIST"},{"key":"16_CR24","first-page":"285","volume":"73","author":"G. Stefanescu","year":"2006","unstructured":"Stefanescu, G.: Interactive systems with registers and voices. Fundamenta Informaticae\u00a073, 285\u2013306 (2006)","journal-title":"Fundamenta Informaticae"},{"key":"16_CR25","unstructured":"Stefanescu, G.: Towards a Floyd logic for interactive rv-systems. In: Proc. ICCP 2006, pp. 169\u2013178. TU Cluj-Napoca (2006)"},{"key":"16_CR26","unstructured":"URL, \n                  \n                    http:\/\/www.petrinets.info\/"},{"key":"16_CR27","unstructured":"URL RODIN tool platform, \n                  \n                    http:\/\/www.event-b.org\/platform.html"},{"key":"16_CR28","first-page":"5","volume":"13","author":"M. Wald\u00e9n","year":"1998","unstructured":"Wald\u00e9n, M., Sere, K.: Reasoning About Action Systems Using the B-Method. FMSD\u00a013, 5\u201335 (1998)","journal-title":"FMSD"},{"key":"16_CR29","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/S0304-3975(97)00154-0","volume":"192","author":"P. Wegner","year":"1998","unstructured":"Wegner, P.: Interactive foundations of computing. TCS\u00a0192, 315\u2013351 (1998)","journal-title":"TCS"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30729-4_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:28:54Z","timestamp":1620113334000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30729-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642307287","9783642307294"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30729-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}