Automating Avionics Certification activities using Formal Methods

Presented as part of the 2019 HCSS conference.

Certification of avionics software is achieved by following a rigorous, prescriptive development process, defined in ​Software Considerations in Airborne Systems and Equipment Certification,  commonly referred to as DO-178C​.This process prescribes software development and verification activities that result in airworthy software. Developing compliant software that adheres to the standard is costly and time consuming; for the most-critical avionics software there are 69 objectives that must be satisfied. Verification and validation of the software accounts for 42 of the objectives and are typically accomplished through a highly manual engineering effort. 

We present an experience report on efforts at Collins Aerospace to automate avionics software certification using formal methods. Peer review and test case generation activities have been automated using open source, SMT-based model checking tools. The tools have been applied to software development in three avionics domains: Crew Alerting Systems, Flight Controls, and Synoptics systems. We discuss the technical aspects of peer review automation and test generation, including pain points, areas for improvement and potential future directions. 

Lucas Wagner is a Principal Research Scientist at Collins Aerospace. His area of expertise is applying formal analysis techniques, particularly model checking, to industrial problems. Mr. Wagner’s background includes developing methods and tools to facilitate the use of formal methods into industrial development processes, the certification of avionics software using model checking, and the qualification of formal methods tools. He has served as the principal investigator on NASA- and AFRL-sponsored efforts to develop and mature formal methods technologies to improve their usage within the avionics community.