{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T00:16:24Z","timestamp":1770336984076,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642340253","type":"print"},{"value":"9783642340260","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34026-0_40","type":"book-chapter","created":{"date-parts":[[2012,9,25]],"date-time":"2012-09-25T21:07:20Z","timestamp":1348607240000},"page":"539-553","source":"Crossref","is-referenced-by-count":6,"title":["Model Learning and Test Generation for Event-B Decomposition"],"prefix":"10.1007","author":[{"given":"Ionut","family":"Dinca","sequence":"first","affiliation":[]},{"given":"Florentin","family":"Ipate","sequence":"additional","affiliation":[]},{"given":"Alin","family":"Stefanescu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"40_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B \u2013 System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"issue":"2","key":"40_CR2","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1002\/spe.1002","volume":"41","author":"R. Silva","year":"2011","unstructured":"Silva, R., Pascal, C., Son Hoang, T., Butler, M.: Decomposition tool for Event-B. Softw., Pract. Exper.\u00a041(2), 199\u2013208 (2011), Plug-in webpage: \n                    \n                      http:\/\/wiki.event-b.org\/index.php\/Event_Model_Decomposition","journal-title":"Softw., Pract. Exper."},{"key":"40_CR3","first-page":"1","volume":"46","author":"T. Hoang Son","year":"2011","unstructured":"Son Hoang, T., Iliasov, A., Silva, R., Wei, W.: A survey on Event-B decomposition. ECEASST\u00a046, 1\u201315 (2011)","journal-title":"ECEASST"},{"key":"40_CR4","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":"40_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-25271-6_7","volume-title":"Formal Methods for Components and Objects","author":"R. Silva","year":"2011","unstructured":"Silva, R., Butler, M.: Shared Event Composition\/Decomposition in Event-B. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 122\u2013141. Springer, Heidelberg (2011)"},{"key":"40_CR6","unstructured":"Abrial, J.-R.: Event model decomposition. Technical Report 626, ETH Zurich (May 2009)"},{"key":"40_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-642-11811-1_24","volume-title":"Abstract State Machines, Alloy, B and Z","author":"T.S. Hoang","year":"2010","unstructured":"Hoang, T.S., Abrial, J.-R.: Event-B Decomposition for Parallel Programs. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 319\u2013333. Springer, Heidelberg (2010)"},{"issue":"6","key":"40_CR8","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","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. STTT\u00a012(6), 447\u2013466 (2010), Tool available online at: \n                    \n                      http:\/\/sourceforge.net\/projects\/rodin-b-sharp","journal-title":"STTT"},{"issue":"8","key":"40_CR9","doi-asserted-by":"publisher","first-page":"1090","DOI":"10.1109\/5.533956","volume":"84","author":"D. Lee","year":"1996","unstructured":"Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines \u2013 A survey. Proc. of the IEEE\u00a084(8), 1090\u20131123 (1996)","journal-title":"Proc. of the IEEE"},{"issue":"16-18","key":"40_CR10","doi-asserted-by":"publisher","first-page":"1770","DOI":"10.1016\/j.tcs.2010.01.030","volume":"411","author":"F. Ipate","year":"2010","unstructured":"Ipate, F.: Bounded sequence testing from deterministic finite state machines. Theoret. Comput. Sci.\u00a0411(16-18), 1770\u20131784 (2010)","journal-title":"Theoret. Comput. Sci."},{"key":"40_CR11","unstructured":"Ipate, F., Dinca, I., Stefanescu, A.: Model learning and test generation using cover automata (submitted, 2012)"},{"key":"40_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-642-30885-7_32","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"I. Dinca","year":"2012","unstructured":"Dinca, I., Ipate, F., Stefanescu, A.: Learn and Test for Event-B \u2013 A Rodin Plugin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol.\u00a07316, pp. 361\u2013364. Springer, Heidelberg (2012), Plug-in webpage: \n                    \n                      http:\/\/wiki.event-b.org\/index.php\/MBT_plugin"},{"issue":"2","key":"40_CR13","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput.\u00a075(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"40_CR14","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.jcss.2011.04.002","volume":"78","author":"F. Ipate","year":"2012","unstructured":"Ipate, F.: Learning finite cover automata from queries. Journal of Computer and System Sciences\u00a078, 221\u2013244 (2012)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1-2","key":"40_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00292-9","volume":"267","author":"C. C\u00e2mpeanu","year":"2001","unstructured":"C\u00e2mpeanu, C., S\u00e2ntean, N., Yu, S.: Minimal cover-automata for finite languages. Theoret. Comput. Sci.\u00a0267(1-2), 3\u201316 (2001)","journal-title":"Theoret. Comput. Sci."},{"key":"40_CR16","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Addison-Wesley (2006)"},{"issue":"3","key":"40_CR17","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"C.S. Pasareanu","year":"2008","unstructured":"Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L\n                  * algorithm to automate assume-guarantee reasoning. Formal Methods in System Design\u00a032(3), 175\u2013205 (2008)","journal-title":"Formal Methods in System Design"},{"key":"40_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/3-540-60218-6_33","volume-title":"CONCUR \u201995 Concurrency Theory","author":"P.S. Thiagarajan","year":"1995","unstructured":"Thiagarajan, P.S.: A Trace Consistent Subset of PTL. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 438\u2013452. Springer, Heidelberg (1995)"},{"key":"40_CR19","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":"40_CR20","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), \n                    \n                      http:\/\/wiki.event-b.org\/index.php\/Modularisation_Plug-in"},{"key":"40_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-87603-8_17","volume-title":"Abstract State Machines, B and Z","author":"M. Poppleton","year":"2008","unstructured":"Poppleton, M.: The Composition of Event-B Models. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 209\u2013222. Springer, Heidelberg (2008), \n                    \n                      http:\/\/wiki.event-b.org\/index.php\/Parallel_Composition_using_Event-B"},{"key":"40_CR22","unstructured":"http:\/\/tinyurl.com\/isola12-with-appendix\n                    \n                    \n                   \u2013 extended version of our paper"},{"key":"40_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/978-3-642-22600-7_16","volume-title":"DCFS 2011","author":"G. Jir\u00e1skov\u00e1","year":"2011","unstructured":"Jir\u00e1skov\u00e1, G., Masopust, T.: State Complexity of Projected Languages. In: Holzer, M. (ed.) DCFS 2011. LNCS, vol.\u00a06808, pp. 198\u2013211. Springer, Heidelberg (2011)"},{"key":"40_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-13977-2_13","volume-title":"Tests and Proofs","author":"J. Julliand","year":"2010","unstructured":"Julliand, J., Stouls, N., Bu\u00e9, P.-C., Masson, P.-A.: Syntactic Abstraction of B Models to Generate Tests. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol.\u00a06143, pp. 151\u2013166. Springer, Heidelberg (2010)"},{"key":"40_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-73066-8_22","volume-title":"Testing of Software and Communicating Systems","author":"M. Shahbaz","year":"2007","unstructured":"Shahbaz, M., Li, K., Groz, R.: Learning and Integration of Parameterized Components Through Testing. In: Petrenko, A., Veanes, M., Tretmans, J., Grieskamp, W. (eds.) TestCom\/FATES 2007. LNCS, vol.\u00a04581, pp. 319\u2013334. Springer, Heidelberg (2007)"},{"key":"40_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-31984-9_14","volume-title":"Fundamental Approaches to Software Engineering","author":"T. Berg","year":"2005","unstructured":"Berg, T., Grinchtein, O., Jonsson, B., Leucker, M., Raffelt, H., Steffen, B.: On the Correspondence Between Conformance Testing and Regular Inference. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol.\u00a03442, pp. 175\u2013189. Springer, Heidelberg (2005)"},{"issue":"3","key":"40_CR27","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1109\/TSE.2009.89","volume":"36","author":"B. Bollig","year":"2010","unstructured":"Bollig, B., Katoen, J.-P., Kern, C., Leucker, M.: Learning communicating automata from MSCs. IEEE Trans. Software Eng.\u00a036(3), 390\u2013408 (2010)","journal-title":"IEEE Trans. Software Eng."},{"key":"40_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1007\/978-3-642-16558-0_53","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"T. Bohlin","year":"2010","unstructured":"Bohlin, T., Jonsson, B., Soleimanifard, S.: Inferring Compact Models of Communication Protocol Entities. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part I. LNCS, vol.\u00a06415, pp. 658\u2013672. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34026-0_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T08:41:26Z","timestamp":1620117686000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34026-0_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642340253","9783642340260"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34026-0_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}