Bridging the Gap Between Informal Requirements and Formal Specifications Using Model Federation.

Software development projects seeking a high level of accuracy reach out to formal methods as early as the requirements engineering phase. However the client perspective of the future system is presented in an informal requirements document. The gap between the formal and informal approaches (and the artifacts used and produced by them) adds further complexity to an already rigorous task of software development. Our goal is to bridge this gap through a fine-grained level of traceability between the client-side informal requirements document to the developer-side formal specifications using a semi-formal modeling technique, model federation. Such a level of traceability can be exploited by the requirements engineering process for performing different actions that involve either or both these informal and formal artifacts. The effort and time consumed in developing such a level of traceability pays back in the later phases of a development project. For example, one can accurately narrow down the requirements responsible for an inconsistency in proof obligations during the analysis phase. We illustrate our approach using a running example from a landing gear system case study.