Computing Science. Refinement-Based Approach to Co-Engineering Requirements and Formal Models.

摘要

Formal modelling is widely recognized 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 affect 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.