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.
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.
- 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.
- 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.
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)
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 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.
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