A system’s requirements drive what features are included in its design. Ensuring that the design adequately reflects the system’s requirements can often be difficult. Formal methods are effective when checking this sort of relationship between artefacts, but only when the artefacts are described formally. However, requirements are often expressed in natural language, and often at a level of detail that is not suitable for direct formalisation [SFM1]. 

Eliciting the system’s requirements and formalising them is a task best completed by a collaboration between those knowledgeable about the system and those knowledgeable about formalisation. But using a formal language during this process can slow down progress, as the systems engineers are taught the intricacies of the formal method, and the formalists try to formalise too much detail too quickly. Thus, semi-formal languages are used as an intermediate between natural- and formal-languages. This avoids slowing down the requirements elicitation process, but still provides enough formalisation to both reduce ambiguities and make the requirements easier to (fully) formalise later on [SFM2]. 

Our tool of choice, the Formal Requirements Elicitation Tool (FRET), uses a structed natural-language called FRETISH as its input language. We manually encode the available natural-language requirements into FRETISH, then FRET automatically translates them into Temporal Logic. FRET is also capable of exporting the requirements as contracts for Simulink diagrams (in a language called CoCoSim).