Building traceable Event-B models from requirements

•We present an approach for incrementally constructing a formal model from informal requirements.•The approach aims to retaining traceability to requirements in models.•We have chosen Event-B to develop the case studies because Event-B is a stepwise formal method which has a platform with various plugins called Rodin.•UML-B is used to enable the development of an Event-B formal model, ERS is used to structure refinements.•To sum up, our approach provides traceability between requirements and the Event-B model and help to construct the Event-B models from requirements.

Bridging the gap between informal requirements and formal specifications is a key challenge in systems engineering. Constructing appropriate abstractions in formal models requires skill and managing the complexity of the relationships between requirements and formal models can be difficult. In this paper we present an approach that aims to address the twin challenges of finding appropriate abstractions and managing traceability between requirements and models. Our approach is based on the use of semi-formal structures to bridge the gap between requirements and Event-B models and retain traceability to requirements in Event-B models. In the stepwise refinement approach, design details are gradually introduced into formal models. Stepwise refinement allows each requirement to be introduced at the most appropriate stage in the development. Our approach makes use of the UML-B and Event Refinement Structures (ERS) approaches. UML-B provides UML graphical notation that enables the development of data structures for Event-B models, while the ERS approach provides a graphical notation to illustrate event refinement structures and assists in the organisation of refinement levels. The ERS approach also combines several constructor patterns to manage control flows in Event-B. The intent of this paper is to harness the benefits of the UML-B and ERS approaches to facilitate constructing Event-B models from requirements and provide traceability between requirements and Event-B models.