Cited By
View all- Hoang TVoisin LWright KSnook CButler M(2024)Semantics Formalisation – From Event-B Contexts to TheoriesRigorous State-Based Methods10.1007/978-3-031-63790-2_14(208-214)Online publication date: 25-Jun-2024
Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion Scheduling
Authors: 
Karla Vanessa Morris Wright, Thai Son Hoang, Colin Snook, Michael ButlerAuthors Info & Claims
Pages 178 - 195
Abstract
The increased complexity of high-consequence digital system designs with intricate interactions between numerous components has placed a greater need on ensuring that the design satisfies its intended requirements. This digital assurance can only come about through rigorous mathematical analysis of the design. This manuscript provides a detailed description of a formal language semantics that can be used for modeling and verification of systems. We use Event-B to build a formalized semantics that supports the construction of triggered enable statecharts with a run-to-completion scheduling. Rodin has previously been used to develop and analyse models using this semantics.
References
[1]
Abrial J-R Modeling in Event-B: System and Software Engineering 2010 Cambridge Cambridge University Press
[2]
Abrial J-R, Butler M, Hallerstede S, Hoang TS, Mehta F, and Voisin L Rodin: an open toolset for modelling and reasoning in Event-B Softw. Tools Technol. Transf. 2010 12 6 447-466
[3]
Barnett J Dahl DA Introduction to SCXML Multimodal Interaction with W3C Standards 2017 Cham Springer 81-107
[4]
Eshuis R Reconciling statechart semantics Sci. Comput. Program. 2009 74 3 65-99
[5]
Harel D Statecharts: a visual formalism for complex systems Sci. Comput. Program. 1987 8 3 231-274
[6]
Harel, D., Gery, E.: Executable object modeling with statecharts. In: Proceedings of IEEE 18th International Conference on Software Engineering, pp. 246–257. IEEE (1996)
[7]
Hoang, T.S., Dghaym, D., Snook, C., Butler, M.: A composition mechanism for refinement-based methods. In: 2017 22nd International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 100–109 (2017)
[8]
Hoang, T.S., Snook, C., Morris, K., Butler, M.: SCXML semantics model in Event-B (2023).
[9]
Hoang TS, Snook C, Dghaym D, Fathabadi AS, and Butler M Masci P, Bernardeschi C, Graziani P, Koddenbrock M, and Palmieri M Building an extensible textual framework for the rodin platform Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops 2023 Cham Springer 132-147
[10]
Lüttgen G, von der Beeck M, and Cleaveland R A compositional approach to statecharts semantics SIGSOFT Softw. Eng. Notes 2000 25 6 120-129
[11]
Morris K, Snook C, Hoang TS, Armstrong R, and Butler M Artho C and Ölveczky PC Refinement of statecharts with run-to-completion semantics Formal Techniques for Safety-Critical Systems 2019 Cham Springer 121-138
[12]
Morris K, Snook C, Hoang TS, Hulette G, Armstrong R, and Butler M Raschke A, Méry D, and Houdek F Refinement and verification of responsive control systems Rigorous State-Based Methods 2020 Cham Springer 272-277
[13]
Morris K, Snook CF, Hoang TS, Hulette GC, Armstrong RC, and Butler MJ Formal verification and validation of run-to-completion style state charts using Event-B Innov. Syst. Softw. Eng. 2022 18 4 523-541
[14]
Snook CF, Butler MJ, Hoang TS, Fathabadi AS, and Dghaym D Masci P, Bernardeschi C, Graziani P, Koddenbrock M, and Palmieri M Developing the UML-B modelling tools Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops 2023 Cham Springer 181-188
[15]
W3C. SCXML specification website (2015). http://www.w3.org/TR/scxml/
Index Terms
- Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion Scheduling
Index terms have been assigned to the content through auto-classification.
Recommendations
Semantics Formalisation – From Event-B Contexts to Theories
Rigorous State-Based MethodsAbstractThe Event-B modelling language has been used to formalise the semantics of other modelling languages such as Time Mobility (TiMo) or State Chart XML (SCXML). Typically, the syntactical elements of the languages are captured as Event-B contexts ...
A UML statecharts semantics with message-passing
SAC '02: Proceedings of the 2002 ACM symposium on Applied computingWe give a formal semantics for one of the main UML diagram types for dynamical system behavior: statechart diagrams. This is the first semantics which explicitly models message-passing between different diagrams. It therefore lays a first foundation for ...
Formalizing the Semantics of UML Statecharts with Z*
CIT '04: Proceedings of the The Fourth International Conference on Computer and Information TechnologyUML is a semi-formal laguage, with a precisely defined syntax and static semantics but with an only informally specified dynamic semantics. UML statechart diagrams are a notation for describing behaviors in the framework of UML. UML statechart diagrams ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Dec 2023
450 pages
ISBN:978-3-031-47962-5
DOI:10.1007/978-3-031-47963-2
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2023.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 04 December 2023
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
Cited By
View all- Hoang TVoisin LWright KSnook CButler M(2024)Semantics Formalisation – From Event-B Contexts to TheoriesRigorous State-Based Methods10.1007/978-3-031-63790-2_14(208-214)Online publication date: 25-Jun-2024
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in