Proving correctness of safety-critical software systems is potentially as important as the development of these systems. Verification tools can be used to automatically analyze a system, but this requires requirements to be specified in a suitable formalism. Currently, requirements are often separately specified in a natural language and subsequently formalized. This is time and effort intensive and error-prone, mostly because the natural language requirements might be ambiguous.

In this research, we present a framework (FRET) that allows users to specify unambiguous requirements in natural language, by using requirement templates that capture patterns between requirements. Furthermore, we discuss its functionality to automatically formalize these requirements into predetermined formalisms.

Through two case studies using ten realistic requirement specifications, we have evaluated this framework in comparison to the current situation of requirements specification and formalization. We found that FRET is currently capable of specifying all of the provided requirements and formalizing 94% of the requirements that could be manually formalized. Furthermore, FRET allows users to specify and formalize requirements in less time and with less effort and specification and formalization in FRET is less error-prone due to the effect of requirement templates on ambiguity, when comparing it to the current situation of requirements specification and formalization. Finally, we have established that two different formalizations of a default template are in fact equivalent to each other. Thus, we are capable of determining whether a template is consistent with regard to its set of formalizations.