Building traceable Event-B models from requirements

Abstract 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