Five years after the official adoption of the new DO-178C/ED-12C standard and its supplements, including the DO-333/ED-216 supplement on formal methods, no avionics-certification project has yet acknowledged using this new supplement. However, formal method technologies do exist that would ease the development of avionics software.
PARIS and NEW YORK. AdaCore has announced the completion of Project Hi-Lite, a joint research project focused on enhancing formal verification for multi-language, open-source software projects that require safety certification. Leveraging Airbus verification methods and industry tools, Project Hi-Lite combined formal proofs with testing and static analysis to improve the development of high integrity software. In the process, the Hi-Lite project also produced the first tools capable of integrating testing and formal verification for Ada and C programs.