Formal model validation through acceptance tests

When formal systems modelling is used as part of the development process, modellers need to understand the requirements in order to create appropriate models, and domain experts need to validate the final models to ensure they fit the needs of stakeholders. A suitable mechanism for such a validation are acceptance tests.In this paper we discuss how the principles of Behaviour-Driven Development (BDD) can be applied to i) formal modelling and ii) validation of behaviour specifications, thus coupling those two tasks. We show how to close the gap between the informal domain specification and the formal model, thus enabling the domain expert to write acceptance tests in a high-level language matching the formal specification.We analyse the applicability of this approach by providing the Gherkin scenarios for an Event-B/iUML-B formal model of a ‘fixed virtual block’ approach to train movement control, developed according to the Hybrid ERTMS/ETCS Level 3 principles specified by the EEIG ERTMS Users Group and presented as a case study on the 6. International ABZ Conference 2018