{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:38Z","timestamp":1781238938673,"version":"3.54.1"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,3,4]],"date-time":"2022-03-04T00:00:00Z","timestamp":1646352000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,4]],"date-time":"2022-03-04T00:00:00Z","timestamp":1646352000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2022,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>State chart notations with \u2018run to completion\u2019 semantics are popular with engineers for designing controllers that react to environment events with a sequence of state transitions but lack formal refinement and rigorous verification methods. State chart models are typically used to design complex control systems that respond to environmental triggers with a sequential process. The model is usually constructed at a concrete level and verified and validated using animation techniques relying on human judgement. Event-B, on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. Abstraction and formal verification provide greater assurance that critical (e.g. safety or security) properties are not violated by the control system. In this paper, we introduce a notion of refinement into a \u2018run to completion\u2019 state chart modelling notation and leverage Event-B\u2019s tool support for theorem proving. We describe the difficulties in translating \u2018run to completion\u2019 semantics into Event-B refinements and suggest a solution. We illustrate our approach and show how models can be validated at different refinement levels using our scenario checker animation tools. We show how critical invariant properties can be verified by proof despite the reactive nature of the system and how behavioural aspects of the system can be verified by testing the expected reactions using a temporal logic, model checking approach. To verify liveness, we outline a proof that the run to completion is deadlock-free and converges to complete the run.<\/jats:p>","DOI":"10.1007\/s11334-021-00416-4","type":"journal-article","created":{"date-parts":[[2022,3,4]],"date-time":"2022-03-04T15:55:15Z","timestamp":1646409315000},"page":"523-541","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Formal verification and validation of run-to-completion style state charts using Event-B"],"prefix":"10.1007","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0146-3176","authenticated-orcid":false,"given":"K.","family":"Morris","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C.","family":"Snook","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"T. S.","family":"Hoang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"G.","family":"Hulette","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R.","family":"Armstrong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"M.","family":"Butler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,3,4]]},"reference":[{"key":"416_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 JR (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge"},{"issue":"6","key":"416_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial JR, Butler M, Hallerstede S, Hoang T, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. Softw Tools Technol Transf 12(6):447\u2013466","journal-title":"Softw Tools Technol Transf"},{"key":"416_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-9668-0_6","volume-title":"Parallel program design: a foundation","author":"KM Chandy","year":"1989","unstructured":"Chandy KM, Misra J (1989) Parallel program design: a foundation. Addison-Wesley, New York"},{"key":"416_CR4","unstructured":"Eclipse Foundation: Sirius project website. https:\/\/eclipse.org\/sirius\/overview.html (2016)"},{"issue":"3","key":"416_CR5","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8(3):231\u2013274. https:\/\/doi.org\/10.1016\/0167-6423(87)90035-9","journal-title":"Sci Comput Program"},{"key":"416_CR6","unstructured":"Hoang, T.S.: An introduction to the Event-B modelling method. In: Industrial deployment of system engineering methods. Springer, pp 211\u2013236 (2013)"},{"key":"416_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0376-0","author":"TS Hoang","year":"2016","unstructured":"Hoang TS, Schneider S, Treharne H, Williams D (2016) Foundations for using linear temporal logic in event-b refinement. Form Asp Comput. https:\/\/doi.org\/10.1007\/s00165-016-0376-0","journal-title":"Form Asp Comput"},{"issue":"4","key":"416_CR8","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 TS, Ostroff JS (2016) The Unit-B method: refinement guided by progress concerns. Softw Syst Model 15(4):1091\u20131116. https:\/\/doi.org\/10.1007\/s10270-015-0456-2","journal-title":"Softw Syst Model"},{"key":"416_CR9","doi-asserted-by":"crossref","unstructured":"Kuppe MA, Lamport L, Ricketts D (2019) The TLA+ toolbox. In: Monahan R, Prevosto V, Proen\u00e7a J (eds) Proceedings fifth workshop on formal integrated development environment, F-IDE@FM 2019, Porto, Portugal, 7th October 2019. EPTCS, vol\u00a0310, pp 50\u201362. https:\/\/doi.org\/10.4204\/EPTCS.310.6","DOI":"10.4204\/EPTCS.310.6"},{"key":"416_CR10","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"2","author":"L Lamport","year":"1977","unstructured":"Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 2:125\u2013143","journal-title":"IEEE Trans Softw Eng"},{"key":"416_CR11","volume-title":"Specifying systems, the TLA+ language and tools for hardware and software engineers","author":"L Lamport","year":"2002","unstructured":"Lamport L (2002) Specifying systems, the TLA+ language and tools for hardware and software engineers. Addison-Wesley, New York"},{"key":"416_CR12","unstructured":"Maraninchi, F.: The Argos language: graphical representation of automata and description of reactive systems. In: IEEE workshop on visual languages (1991)"},{"key":"416_CR13","unstructured":"MATLAB: 9.7.0.1190202 (R2019b). The MathWorks Inc., Natick, Massachusetts"},{"key":"416_CR14","unstructured":"Morris K, Snook C (2016) Reconciling SCXML statechart representations and Event-B lower level semantics. In: HCCV: workshop on high-consequence control verification. http:\/\/www.sandia.gov\/hccv\/_assets\/documents\/HCCV_2016_Morris.pdf"},{"key":"416_CR15","first-page":"121","volume-title":"Formal techniques for safety-critical systems","author":"K Morris","year":"2019","unstructured":"Morris K, Snook C, Hoang TS, Armstrong R, Butler M (2019) Refinement of statecharts with run-to-completion semantics. In: Artho C, \u00d6lveczky PC (eds) Formal techniques for safety-critical systems. Springer, Cham, pp 121\u2013138"},{"key":"416_CR16","doi-asserted-by":"crossref","unstructured":"Morris K, Snook C, Hoang TS, Hulette G, Armstrong R, Butler, M.: Formal verification of run-to-completion style statecharts using event-b. In: Muccini H (ed) Software architecture. ECSA 2020. Communications in computer and information science, vol 1269. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-59155-7_24","DOI":"10.1007\/978-3-030-59155-7_24"},{"key":"416_CR17","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-030-48077-6_23","volume-title":"Rigorous state-based methods","author":"K Morris","year":"2020","unstructured":"Morris K, Snook C, Hoang TS, Hulette G, Armstrong R, Butler M (2020) Refinement and verification of responsive control systems. In: Raschke A, M\u00e9ry D, Houdek F (eds) Rigorous state-based methods. Springer, Cham, pp 272\u2013277"},{"issue":"1","key":"416_CR18","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C Snook","year":"2006","unstructured":"Snook C, Butler M (2006) UML-B: Formal modeling and design aided by UML. ACM Trans Softw Eng Methodol 15(1):92\u2013122. https:\/\/doi.org\/10.1145\/1125808.1125811","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"416_CR19","doi-asserted-by":"crossref","unstructured":"Snook C, Hoang TS, Dghaym D, Fathabadi AS, Butler M (2020) Domain-specific scenarios for refinement-based methods. (to be published in) J Syst Archit","DOI":"10.1016\/j.sysarc.2020.101833"},{"issue":"15","key":"416_CR20","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.scico.2018.10.005","volume":"170","author":"E Syriani","year":"2019","unstructured":"Syriani E, Sousa V, L\u00facio L (2019) Structure and behavior preserving statecharts refinements. Sci Comput Program 170(15):45\u201379. https:\/\/doi.org\/10.1016\/j.scico.2018.10.005","journal-title":"Sci Comput Program"},{"key":"416_CR21","unstructured":"W3C (2015) State chart XML SCXML: state machine notation for control abstraction. http:\/\/www.w3.org\/TR\/scxml\/"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-021-00416-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-021-00416-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-021-00416-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,14]],"date-time":"2022-11-14T09:16:04Z","timestamp":1668417364000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-021-00416-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,4]]},"references-count":21,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["416"],"URL":"https:\/\/doi.org\/10.1007\/s11334-021-00416-4","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,3,4]]},"assertion":[{"value":"5 January 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 August 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 March 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}