Formal Verification Tool Evaluation For Unmanned Aircraft Containing Complex Functions

• Main Authors: Herencia-Zapana, Heber, Lopez, James, Gallagher, Glen, Meng, Baoluo, Patterson, Cameron, Maalolan, Lakshman
• Format: Conference Proceeding
• Language: English
• Subjects: Certification; F3269-17; Formal methods; Germanium; Monitoring; Ontologies; Safety; safety critical systems; Software; UAS; V&V process
• ISSN: 2155-7209
• DOI: 10.1109/DASC50938.2020.9256529

The expected proliferation of UAS in the NAS requires technologies that ensure safe operation. There is significant interest from industry and civil aviation authorities to have a standard practice to enable flight operations for UAS containing flight safety critical functions which are too costly to certify. Developing a certification path for these UAS technologies could advance safety of UAS operating in the NAS. In response to this need ASTM released standard F3269-17 in 2018. This standard proposes a run-time assurance architecture whereby an untrusted or non-pedigreed and therefore non-certified flight safety critical function (complex function) can be included in a UAS avionics system that can be certified. GE Aviation is developing an avionics solution intended for safe operation of UAS. As part of ensuring safe operation of UAS GE Aviation's avionics implements a runtime safety assurance (RTA) system that follows the guidelines laid out in the ASTM F3269-17 standard. Formal methods-based verification and validation (V&V) tools hold great promise for addressing the exploding cost of performing V&V on flight safety critical systems that include software. However, there are very few examples demonstrating a side-by-side comparison of the traditional V&V approach and a V&V approach where formal methods-based tools are used at appropriate steps in the process. This paper presents a side-by-side comparison of a complete V&V process for the RTA using both traditional and formal methods-based V&V and shows the benefits of formal tools applied at various early stages of the V&V process. More specifically this paper shows a comparison for the generation of the following evidence for the RTA: Requirements analysis, test case generation, and prof that requirements are fully implemented by the select sub-systems and/or components architecture.