Opportunities and challenges for formal methods tools in the certification of avionics software

Formal methods tools, whose underlying principles are based on mathematics and formal logic, are considered one of the most effective and rigorous means of verifying system properties and assuring the absence of undesirable system behavior. The use of such tools seem to squarely fit the needs of those aiming to develop and certify avionic software as per the DO-178C standard, the set of objectives laid out by FAA to achieve a high level of confidence on the systems. However, our recent work on a NASA-funded research project revealed that there are practical considerations and additional complexities involved in using formal method tools to provide the level of assurance as exemplified by the DO-178C. In this paper we discuss one of the key concerns with formal tools: its soundness — the characteristic of a tool to never permit the verified system property be declared true when it is actually not true. We explored two major classes of formal methods tools — namely model checkers and static analyzers — and observed several threats to their soundness such as tool fallacies and failure modes that could lead to misplaced confidence in the verified system. We present various strategies to mitigate them, including an assurance case framework to verify that potential risks are all mitigated. The intent of this paper is not to discourage but encourage scrupulous use of formal tools to certify critical avionic software by being wary of the subtle but serious issues that may be overlooked.