{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:06:28Z","timestamp":1781651188820,"version":"3.54.5"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031945328","type":"print"},{"value":"9783031945335","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T00:00:00Z","timestamp":1748822400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T00:00:00Z","timestamp":1748822400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-94533-5_8","type":"book-chapter","created":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T19:32:30Z","timestamp":1756668750000},"page":"124-142","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Translating Event-B Models and Development Proofs to TLA+"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-3020-3660","authenticated-orcid":false,"given":"Anne","family":"Grieu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4179-6063","authenticated-orcid":false,"given":"Jean-Paul","family":"Bodeveix","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5387-6805","authenticated-orcid":false,"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,6,2]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"8_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR 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":"6","key":"8_CR3","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR 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. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0145-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Berkani, K., Dubois, C., Faivre, A., Falampin, J.: Validation des r\u00e8gles de base de l\u2019atelier B. Tech. Sci. Informatiques 23(7), 855\u2013878 (2004). https:\/\/doi.org\/10.3166\/TSI.23.855-878","DOI":"10.3166\/TSI.23.855-878"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-030-77543-8_5","volume-title":"Rigorous State-Based Methods","author":"J-P Bodeveix","year":"2021","unstructured":"Bodeveix, J.-P., Filali, M.: Event-B formalization of Event-B contexts. In: Raschke, A., M\u00e9ry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 66\u201380. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_5"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-32759-9_14","volume-title":"FM 2012: Formal Methods","author":"D Cousineau","year":"2012","unstructured":"Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA+ proofs. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 147\u2013154. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_14"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-662-43652-3_26","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Delahaye","year":"2014","unstructured":"Delahaye, D., Dubois, C., March\u00e9, C., Mentr\u00e9, D.: The BWare project: building a proof platform for the automated verification of b proof obligations. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 290\u2013293. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_26"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/J.SCICO.2016.04.014","volume":"131","author":"D Hansen","year":"2016","unstructured":"Hansen, D., Leuschel, M.: Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131, 109\u2013125 (2016). https:\/\/doi.org\/10.1016\/J.SCICO.2016.04.014","journal-title":"Sci. Comput. Program."},{"key":"8_CR10","unstructured":"Hoang, T.S.: An introduction to the Event-B modelling method. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 211\u2013236. Springer, Heidelberg (2013). http:\/\/www.springer.com\/computer\/swe\/book\/978-3-642-33169-5"},{"issue":"4","key":"8_CR11","doi-asserted-by":"publisher","first-page":"1091","DOI":"10.1007\/S10270-015-0456-2","volume":"15","author":"S Hudon","year":"2016","unstructured":"Hudon, S., Hoang, T.S., Ostroff, J.S.: The Unit-B method: refinement guided by progress concerns. Softw. Syst. Model. 15(4), 1091\u20131116 (2016). https:\/\/doi.org\/10.1007\/S10270-015-0456-2","journal-title":"Softw. Syst. Model."},{"key":"8_CR12","unstructured":"Lamport, L.: TLA$$^{+}$$ version 2 a preliminary guide. https:\/\/lamport.azurewebsites.net\/tla\/tla2-guide.pdf. Accessed 18 Feb 2025"},{"key":"8_CR13","unstructured":"Lamport, L.: Specifying Systems: The TLA$$^{+}$$ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., USA (2002)"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Lecomte, T., D\u00e9harbe, D., Fournier, P., Oliveira, M.: The CLEARSY safety platform: 5 years of research, development and deployment. Sci. Comput. Program. 199, 102524 (2020). https:\/\/doi.org\/10.1016\/J.SCICO.2020.102524","DOI":"10.1016\/J.SCICO.2020.102524"},{"issue":"2","key":"8_CR15","doi-asserted-by":"publisher","first-page":"835","DOI":"10.1109\/TR.2022.3219649","volume":"73","author":"P Rivi\u00e8re","year":"2024","unstructured":"Rivi\u00e8re, P., Singh, N.K., A\u00eft-Ameur, Y.: Reflexive Event-B: semantics and correctness the EB4EB framework. IEEE Trans. Reliab. 73(2), 835\u2013850 (2024). https:\/\/doi.org\/10.1109\/TR.2022.3219649","journal-title":"IEEE Trans. Reliab."},{"key":"8_CR16","unstructured":"Verdier, G., Voisin, L.: Context instantiation plug-in: a new approach to genericity in Rodin (2021). https:\/\/eprints.soton.ac.uk\/449887\/1\/proceedings.pdf. Accessed 19 Feb 2025"}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-94533-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T00:19:55Z","timestamp":1757463595000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-94533-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,2]]},"ISBN":["9783031945328","9783031945335"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-94533-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,2]]},"assertion":[{"value":"2 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"D\u00fcsseldorf","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz-conf.org\/site\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}