A Formal Framework for the Formalization of Informal Requirements

Systems’ requirements are usually written in a natural language since it generally means a greater understanding among the various stakeholders. However, using an informal language potentially gives rise to interpretation problems, which are to be resolved prior to using (automated) verification techniques. This article tackles an important issue pertaining to requirement engineering: how to guide and help requirements’ formalization? In order to support the formalization process, we propose a methodology based on a formal structure, which is the corner stone of the refinement process. The operating mode of the refinement process is highly iterative: the aforementioned structure is constructed incrementally until its validity is formally obtained. Although this process is formally backed up, it is a fundamentally subjective one, which means that interpretation errors can still occur. In case of errors, it is essential to be able to backtrack refinements until an interpretation error is found. This is why we require that each refinement be associated with a justification which may subsequently be analyzed in case an error occurred during the verification phase. This formalization process was designed to be used alongside an (unspecific) engineering process, in charge of the implementation. Once the formalization is complete, it is checked against the implementation using testing techniques, or directly against an implementation model via model-checking.