A Requirements-Driven Methodology: Formal Modelling and Verification of an Aircraft Engine Controller

The formal verification of software systems often requires the integration of multiple tools and techniques. To ensure the accuracy of any verification done and to ensure the applicability of formal methods to industrial use cases, traceability must be maintained throughout the process so that it is clear what the requirements for the system are and how they are fulfilled. We propose a three-phase methodology for formal verification with the aim of ensuring traceability, built around the Formal Requirements Elicitation Tool (FRET). Our current case study applies this methodology to the use of FRET, Simulink and Event-B for the verification of the software controller for a civilian aircraft engine.