Conference Publication Details
Mandatory Fields
Sheridan O.;Monahan R.;Luckcuck M.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A Requirements-Driven Methodology: Formal Modelling and Verification of an Aircraft Engine Controller
Optional Fields
Event-B Formal methods FRET Software verification
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.
Grant Details