This workflow  begins with a semi-formal requirements elicitation phase, supported by the Formal Requirements Elicitation Tool (FRET), and leads to formal verification using these requirements . There are two ‘legs’ of the verification part of the workflow, one that integrates the verification into a Simulink diagram, and another based on more traditional formal verification using theorem proving and/or model checking.  

The semi-formal language used by FRET (called FRETISH) enables the requirements elicitation process to reduce or remove the ambiguity of natural-language requirements without requiring participants to learn a fully formal language. FRET already integrates with a toolchain for producing contracts for Simulink diagrams, which are checked during simulations. To perform more exhaustive model checking or theorem proving, we develop translations from FRETISH into other formalisms for formal verification. One such formalism we have focused on is Event-B, via the Rodin platform. We have developed a formal system model, using the Simulink model and FRETISH requirements as a basis, which allows us to perform model checking and theorem proving to verify the behaviour of the system.