Refinement-based Approach to Co-engineering Requirements and Formal Models

Formal modelling is widely recognised to contribute to the rigour and comprehensiveness of requirements. At the same time, a formal specification does not offer the flexibility and legibility of informal requirements, expected by system designers and software engineers. In this paper we propose a method and a supporting platform for tightly integrated co-engineering of a requirements document and the corresponding formal specification. We show that bi-directional transformation between requirements and models affects the practice of requirements construction by, arguably, bringing additional rigour and discipline while retaining the flexibility of informal requirements. We report on the experience of applying the OSLC framework to integrate a requirements engineering tool with the Rodin modelling and verification environment. A prototype implementation illustrates the main steps of the proposed approach.

Alexei Iliasov, David Adjepon-Yamoah, Alexander Romanovsky (Newcastle University), Linas Laibinis, Elena Troubitsyna (Åbo Akademi University): Refinement-based Approach to Co-engineering Requirements and Formal Models