Research



Behaviour Driven Formal Modelling


Behaviour driven formal model development (BDFMD) enables domain engineers to influence and validate mathematically precise and verified specifications. We have developed a process where manually authored scenarios are used initially to support the requirements and help the modeller. The same scenarios are used to verify behavioural properties of the model. The model is then mutated (using the MoMuT tools from Austrian Institute of Technology) to automatically generate scenarios that have a more complete coverage than the manual ones. These automatically generated scenarios are used to animate the model in a final acceptance stage.


Butler, M. et al., "Behaviour-Driven Formal Model Development of the ETCS Hybrid Level 3," 2019 24th International Conference on Engineering of Complex Computer Systems (ICECCS), Guangzhou, China, 2019, pp. 97-106, doi: 10.1109/ICECCS.2019.00018.

Figure 1 - Process for Behaviour Driven Formal Modelling

Domain-Specific Scenarios for Refinement-based Methods


Formal methods use abstraction and rigorously verified refinement to manage the design of complex systems, ensuring that they satisfy important invariant properties. However, formal verification is not sufficient: models must also be tested to ensure that they behave according to the informal requirements and validated by domain experts who may not be expert in formal modelling. This can be satisfied by scenarios that complement the requirements specification. The model can be animated to check whether the scenario is feasible in the model and that the model reaches the states expected in the scenario. However, there are two problems with this approach.

  1. The natural language used to describe the scenarios is often verbose, ambiguous and therefore difficult to understand; especially if the modeller is not a domain expert.
  2. Provided scenarios are typically at the most concrete level corresponding to the full requirements and cannot be used until all the refinements have been completed in the model.
A precise and concise domain specific language can be used for writing these abstract scenarios in a style that can be easily understood by the domain expert (for validation purposes) as well as the modeller (for behavioural verification) and can be used as the persistence for automated tool support. We propose two alternative approaches to using scenarios during formal modelling: A method of refining scenarios before the model is refined so that the scenarios guide the modelling, and a method of abstracting scenarios from provided concrete ones so that they can be used to test early refinements of the model. Tool support for managing the animation of scenarios is provided by the `Scenario Checker' plugin.

Snook, C., Hoang, T.S., Dghaym, D., Salehi-Fathabadi, A., Butler, M.: Domain Specific Scenarios for Refinement-based Methods. Journal of Systems Architecture (to be published), https://doi.org/10.1016/j.sysarc.2020.101833 (2020)


Figure 2 - The Scenario Checker re-playing a scenario



Text Editing and Persistence - CamilleX, xUML-B


Rodin model files are based on XML which is loaded into memory as an object structure for editing and manipulation. While this works well for most modelling tools, some disadvantages remain:

  • Editing operations such as cut and paste are less effective than with a pure text representation.
  • Comparison tools are less effective than for text comparison.
  • Storing models in shared repositories is cumbersome.
CamilleX is a new XText-based front-end for Event-B models which provides a textual representation and persistence. CamilleX supports two types of textual files XMachine and XContext, which in turn will be automatically translated to the corresponding Rodin Event-B components (machine and context). A facility for translating from Rodin Event-B components to CamilleX components can be invoked manually. The overall process can be seen in Figure 2.


Figure 3 - Overview of CamilleX

CamilleX provides a front-end editor based on XText. XText is an open source framework for developing modelling languages based on the Eclipse Modelling Framework (EMF).

Records extension - The CamilleX plug-in is extended so that it not only supports standard Event-B, but also provides support for record data structures. Records are translated to standard Event-B when the model is saved, hence it is not required to be processed by the Rodin tools.


Figure 4 - Xtext and context components

Spark Code Generation


Ensuring properties of safety- and security-critical systems is paramount. Event-B is a formal modelling method which enables the design of systems, using mathematical proofs ensuring the conformity of the system to declared safety requirements. SPARK is a programming language making use of static analysis tools which verify written code correctly implements the properties of the system as specified in the form of written proof annotations (e.g., pre- and post-conditions). SPARK has been used in many industry-scale projects to implement safety-critical software. However, manually writing SPARK proof annotations can be time-consuming and tedious. Our motivation is to develop a tool-supported approach to translate an Event-B model into a SPARK package, including proof annotations and other structures, from which manually written SPARK code can be verified, hence ensuring the correct behaviour of the software. One aim is to cover as much as possible the Event-B mathematical language that can be translated into SPARK. Event-B sets and relations are translated as SPARK Boolean arrays. A library is built to support the translation. Furthermore, properties of the systems such as axioms and invariants are translated and embedded in SPARK as pre- and post-conditions. These properties, in particular invariance properties, are often global system properties ensuring the safety and consistency of the overall system, and are often difficult to be discovered. Using these conceptual translation rules, we have developed a a plug-in for the Rodin platform. Our approach can be summarised as follows:

  • One SPARK package for the Event-B machine
  • Invariants are translated as expression functions
  • Each event translated as a procedure with the same set of parameters
    • Global aspect: compute from guards and actions of the event.
    • Depends aspect: compute from the actions of the event.
    • Pre-condition: generated from all axioms, invariants and the guards of the event
    • Post-condition: generated from all axioms, invariants and the actions of the event.
    • Procedure body: generated from the actions of the event
In terms of translating sets and relations, we have also considered different approaches including using functional sets and formal ordered sets. Our experiment shows that these representations have limited support for set and relational operators and did not work well with the SPARK provers. We plan to investigate the usage of Boolean arrays for sets and relations in SPARK as a mechanism for reasoning about abstract concepts using SMT solvers together with University of Oxford and Altran.