The 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 while the semantical elements are formalised in Event-B machines. An alternative for capturing a modelling language’s semantics is to use the Theory plug-in to build datatypes capturing the syntactical elements of the language and operators to represent the various semantical aspects of the language. This paper draws on our experience on the statemanchines (part of SCXML) to compare the two approaches in terms of modelling efforts.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{HoangVWSB24,
author = {Thai Son Hoang and
Laurent Voisin and
Karla Vanessa Morris Wright and
Colin F. Snook and
Michael J. Butler},
editor = {Silvia Bonfanti and
Angelo Gargantini and
Michael Leuschel and
Elvinia Riccobene and
Patrizia Scandurra},
title = {Semantics Formalisation - From Event-B Contexts to Theories},
booktitle = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14759},
pages = {208--214},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-63790-2\_14},
doi = {10.1007/978-3-031-63790-2\_14},
timestamp = {Thu, 04 Jul 2024 22:05:23 +0200},
biburl = {https://dblp.org/rec/conf/zum/HoangVWSB24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}