{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:53:58Z","timestamp":1742918038979,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031671135"},{"type":"electronic","value":"9783031671142"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-67114-2_14","type":"book-chapter","created":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:42:47Z","timestamp":1725507767000},"page":"346-374","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Semantics Formalisation \u2013 Modelling and\u00a0Proving Strategies Using Event-B Versus Theories"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4095-0732","authenticated-orcid":false,"given":"Thai Son","family":"Hoang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0210-0983","authenticated-orcid":false,"given":"Colin","family":"Snook","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0146-3176","authenticated-orcid":false,"given":"Karla Vanessa","family":"Morris Wright","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2426-0101","authenticated-orcid":false,"given":"Laurent","family":"Voisin","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4642-5373","authenticated-orcid":false,"given":"Michael","family":"Butler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,1]]},"reference":[{"key":"14_CR1","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. Cambridge University Press, Cambridge (2010)"},{"issue":"6","key":"14_CR2","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., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Softw. Tools Technol. Transf."},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-319-42816-1_5","volume-title":"Multimodal Interaction with W3C Standards","author":"J Barnett","year":"2017","unstructured":"Barnett, J.: Introduction to SCXML. In: Dahl, D. (ed.) Multimodal Interaction with W3C Standards, pp. 81\u2013107. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-42816-1_5"},{"key":"14_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-39698-4_5","volume-title":"Theories of Programming and Formal Methods","author":"MJ Butler","year":"2013","unstructured":"Butler, M.J., Maamria, I.: Practical theory extension in Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 67\u201381. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-642-39698-4_5"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Ciobanu, G., Hoang, T.S., Stefanescu, A.: From TiMo to Event-B: event-driven timed mobility. In: 2014 19th International Conference on Engineering of Complex Computer Systems, Tianjin, China, 4\u20137 August 2014, pp. 1\u201310. IEEE Computer Society (2014). https:\/\/doi.org\/10.1109\/ICECCS.2014.10","DOI":"10.1109\/ICECCS.2014.10"},{"key":"14_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-030-02146-7_7","volume-title":"Formal Aspects of Component Software","author":"S Foster","year":"2018","unstructured":"Foster, S., Baxter, J., Cavalcanti, A., Miyazawa, A., Woodcock, J.: Automating verification of state machines with reactive designs and Isabelle\/UTP. In: Bae, K., \u00d6lveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 137\u2013155. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02146-7_7"},{"key":"14_CR7","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102510","volume":"197","author":"S Foster","year":"2020","unstructured":"Foster, S., Baxter, J., Cavalcanti, A., Woodcock, J., Zeyda, F.: Unifying semantic foundations for automated verification tools in Isabelle\/UTP. Sci. Comput. Program. 197, 102510 (2020). https:\/\/doi.org\/10.1016\/j.scico.2020.102510","journal-title":"Sci. Comput. Program."},{"key":"14_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-031-26236-4_11","volume-title":"SEFM 2022","author":"TS Hoang","year":"2022","unstructured":"Hoang, T.S., Snook, C.F., Dghaym, D., Fathabadi, A.S., Butler, M.J.: Building an extensible textual framework for the Rodin platform. In: Masci, P., Bernardeschi, C., Graziani, P., Koddenbrock, M., Palmieri, M. (eds.) SEFM 2022. LNCS, vol. 13765, pp. 132\u2013147. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-26236-4_11"},{"key":"14_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-031-63790-2_14","volume-title":"ABZ 2024","author":"TS Hoang","year":"2024","unstructured":"Hoang, T.S., Voisin, L., Morris Wright, K.V., Snook, C.F., Butler, M.J.: Semantics formalisation - from Event-B contexts to theories. In: Riccobene, E., Leuschel, M., Bonfanti, S., Gargantini, A. (eds.) ABZ 2024. LNCS, vol. 14759, pp. 208\u2013214. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63790-2_14"},{"key":"14_CR10","unstructured":"Hoang, T.S., Voisin, L., Salehi, A., Butler, M.J., Wilkinson, T., Beauger, N.: Theory plug-in for Rodin 3.x. CoRR abs\/1701.08625 (2017). http:\/\/arxiv.org\/abs\/1701.08625"},{"key":"14_CR11","unstructured":"Hoare, C., Jifeng, H.: Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice Hall (1998). https:\/\/books.google.com\/books?id=WpdQAAAAMAAJ"},{"key":"14_CR12","series-title":"Springer Proceedings in Advanced Robotics","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-319-73008-0_36","volume-title":"Distributed Autonomous Robotic Systems","author":"W Li","year":"2018","unstructured":"Li, W., Miyazawa, A., Ribeiro, P., Cavalcanti, A., Woodcock, J., Timmis, J.: From formalised state machines to implementations of robotic controllers. In: Gro\u00df, R., et al. (eds.) Distributed Autonomous Robotic Systems. Springer Proceedings in Advanced Robotics, vol. 6, pp. 517\u2013529. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73008-0_36"},{"key":"14_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-031-33170-1_19","volume-title":"NFM 2023","author":"P Riviere","year":"2023","unstructured":"Riviere, P., Singh, N.K., Ameur, Y.A., Dupont, G.: Formalising liveness properties in Event-B with the reflexive EB4EB framework. In: Rozier, K.Y., Chaudhuri, S. (eds.) NFM 2023. LNCS, vol. 13903, pp. 312\u2013331. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_19"},{"key":"14_CR14","unstructured":"Verdier, G., Voisin, L.: Context instantiation plug-in: a new approach to genericity in Rodin. https:\/\/wiki.event-b.org\/images\/RodinWorkshop2021_Context_instantiation_plug-in.pdf. Rodin Workshop 2021"},{"key":"14_CR15","unstructured":"W3C: SCXML specification website (2015). http:\/\/www.w3.org\/TR\/scxml\/"},{"key":"14_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-031-40436-8_2","volume-title":"Theories of Programming and Formal Methods","author":"J Woodcock","year":"2023","unstructured":"Woodcock, J., Cavalcanti, A., Foster, S., Oliveira, M., Sampaio, A., Zeyda, F.: UTP, circus, and Isabelle. In: Bowen, J.P., Li, Q., Xu, Q. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 14080, pp. 19\u201351. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-40436-8_2"},{"key":"14_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-031-47963-2_12","volume-title":"ICTAC 2023","author":"KVM Wright","year":"2023","unstructured":"Wright, K.V.M., Hoang, T.S., Snook, C.F., Butler, M.J.: Formal language semantics for triggered enable statecharts with a run-to-completion scheduling. In: \u00c1brah\u00e1m, E., Dubslaff, C., Tarifa, S.L.T. (eds.) ICTAC 2023. LNCS, vol. 14446, pp. 178\u2013195. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47963-2_12"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Yan, F., Foster, S., Habli, I.: Automated compositional verification for robotic state machines using Isabelle\/HOL. In: A\u00eft-Ameur, Y., Khendek, F., M\u00e9ry, D. (eds.) 27th International Conference on Engineering of Complex Computer Systems, ICECCS 2023, Toulouse, France, 14\u201316 June 2023, pp. 167\u2013176. IEEE (2023). https:\/\/doi.org\/10.1109\/ICECCS59891.2023.00029","DOI":"10.1109\/ICECCS59891.2023.00029"},{"key":"14_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-031-17244-1_24","volume-title":"ICFEM 2022","author":"K Ye","year":"2022","unstructured":"Ye, K., Foster, S., Woodcock, J.: Formally verified animation for RoboChart using interaction trees. In: Riesco, A., Zhang, M. (eds.) ICFEM 2022. LNCS, vol. 13478, pp. 404\u2013420. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17244-1_24"}],"container-title":["Lecture Notes in Computer Science","The Application of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-67114-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:45:56Z","timestamp":1725507956000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-67114-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031671135","9783031671142"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-67114-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}