Semantics Formalisation – Modelling and Proving Strategies Using Event-B Versus Theories

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 of the Rodin platform to build algebraic datatypes capturing the syntactical elements of the language and operators to represent the various semantical aspects of the language. We take a closer look at the design of the proof rules supporting the datatypes and operators for reasoning and suggest improvements for the Theory plug-in. We use SCXML as an example modelling language for formalisation to compare the two approaches in terms of modelling and proving efforts.