{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:01:37Z","timestamp":1742976097003,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319478456"},{"type":"electronic","value":"9783319478463"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47846-3_20","type":"book-chapter","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T02:53:57Z","timestamp":1476413637000},"page":"313-328","source":"Crossref","is-referenced-by-count":3,"title":["An Event-B Development Process for the Distributed BIP Framework"],"prefix":"10.1007","author":[{"given":"Badr","family":"Siala","sequence":"first","affiliation":[]},{"given":"Mohamed Tahar","family":"Bhiri","sequence":"additional","affiliation":[]},{"given":"Jean-Paul","family":"Bodeveix","sequence":"additional","affiliation":[]},{"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,15]]},"reference":[{"unstructured":"Java 10, today! http:\/\/www.eclipse.org\/xtend\/ . Accessed 16 Jan 2006","key":"20_CR1"},{"unstructured":"Language engineering for everyone! https:\/\/eclipse.org\/Xtext . Accessed 16 Jan 2006","key":"20_CR2"},{"key":"20_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"issue":"1\u20132","key":"20_CR4","first-page":"1","volume":"77","author":"J-R Abrial","year":"2007","unstructured":"Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundam. Inf. 77(1\u20132), 1\u201328 (2007)","journal-title":"Fundam. Inf."},{"issue":"3","key":"20_CR5","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.-H., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41\u201348 (2011)","journal-title":"IEEE Softw."},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1007\/978-3-540-45236-2_7","volume-title":"FME 2003: Formal Methods","author":"D Bert","year":"2003","unstructured":"Bert, D., Boulm\u00e9, S., Potet, M.-L., Requet, A., Voisin, L.: Adaptable translator of B specifications to embedded C programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 94\u2013113. Springer, Heidelberg (2003)"},{"unstructured":"Butler, M.: A CSP approach to action systems. Ph.D. thesis, Oxford University (1992)","key":"20_CR7"},{"unstructured":"Clearsy. Bart (b automatic refinement tool). http:\/\/tools.clearsy.com\/wp-content\/uploads\/sites\/8\/resources\/BART_GUI_User_Manual.pdf","key":"20_CR8"},{"unstructured":"Edmunds, A., Butler, M.: Tasking Event-B: An extension to Event-B for generating concurrent code. Event Dates: 2nd April 2011, February 2011","key":"20_CR9"},{"doi-asserted-by":"crossref","unstructured":"Edmunds, A., Butler, M.J., Maamria, I., Silva, R., Lovell, C.: Event-B code generation: type extension with theories. In: ABZ Proceedings, pp. 365\u2013368 (2012)","key":"20_CR10","DOI":"10.1007\/978-3-642-30885-7_33"},{"issue":"1","key":"20_CR11","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10270-013-0323-y","volume":"14","author":"Y Falcone","year":"2015","unstructured":"Falcone, Y., Jaber, M., Nguyen, T.-H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation. Softw. Syst. Model. 14(1), 173\u2013199 (2015)","journal-title":"Softw. Syst. Model."},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/978-3-319-10181-1_20","volume-title":"Integrated Formal Methods","author":"A F\u00fcrst","year":"2014","unstructured":"F\u00fcrst, A., Hoang, T.S., Basin, D., Desai, K., Sato, N., Miyazaki, K.: Code generation for Event-B. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 323\u2013338. Springer, Heidelberg (2014)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/978-3-662-43652-3_20","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A F\u00fcrst","year":"2014","unstructured":"F\u00fcrst, A., Hoang, T.S., Basin, D., Sato, N., Miyazaki, K.: Formal system modelling using abstract data types in Event-B. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 222\u2013237. Springer, Heidelberg (2014)"},{"unstructured":"Jaber, M.: Centralized and Distributed Implementations of Correct-by-construction Component-based Systems by using Source-to-source Transformations in BIP. Theses, Universit\u00e9 Joseph-Fourier - Grenoble I, October 2010","key":"20_CR14"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/11921240_1","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"T Nipkow","year":"2006","unstructured":"Nipkow, T.: Verifying a hotel key card system. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 1\u201314. Springer, Heidelberg (2006)"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/978-3-642-33826-7_6","volume-title":"Software Engineering and Formal Methods","author":"A Salehi Fathabadi","year":"2012","unstructured":"Salehi Fathabadi, A., Butler, M., Rezazadeh, A.: A systematic approach to atomicity decomposition in Event-B. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 78\u201393. Springer, Heidelberg (2012)"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-10373-5_24","volume-title":"Formal Methods and Software Engineering","author":"R Silva","year":"2009","unstructured":"Silva, R., Butler, M.: Supporting reuse of Event-B developments through generic instantiation. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 466\u2013484. Springer, Heidelberg (2009)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 122\u2013141. Springer, Heidelberg (2011)"},{"issue":"2","key":"20_CR19","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1002\/spe.1002","volume":"41","author":"R Silva","year":"2011","unstructured":"Silva, R., Pascal, C., Hoang, T.S., Butler, M.: Decomposition tool for Event-B. Softw. Pract. Experience 41(2), 199\u2013208 (2011)","journal-title":"Softw. Pract. Experience"},{"key":"20_CR20","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/978-1-4471-5260-6_7","volume-title":"Using Event-B for Critical Device Software Systems","author":"NK Singh","year":"2013","unstructured":"Singh, N.K.: EB2ALL: an automatic code generation tool. In: Singh, N.K. (ed.) Using Event-B for Critical Device Software Systems, pp. 105\u2013141. Springer, London (2013)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47846-3_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T21:08:04Z","timestamp":1498338484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47846-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319478456","9783319478463"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47846-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}