TY - JOUR
T1 - Opportunities and challenges for formal methods tools in the certification of avionics software
AU - Bhatt, Devesh
AU - Hall, Brendan
AU - Murugesan, Anitha
AU - Oglesby, David
AU - Bush, Eric
AU - Engstrom, Eric
AU - Mueller, Joseph
AU - Pelican, Michael
N1 - Publisher Copyright:
© 2017 IEEE.
PY - 2017
Y1 - 2017
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85042360958&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85042360958&partnerID=8YFLogxK
U2 - 10.1109/AERO.2017.7943664
DO - 10.1109/AERO.2017.7943664
M3 - Conference article
AN - SCOPUS:85042360958
SN - 1095-323X
VL - 2017-June
SP - 1
EP - 20
JO - IEEE Aerospace Conference Proceedings
JF - IEEE Aerospace Conference Proceedings
T2 - 2017 IEEE Aerospace Conference, AERO 2017
Y2 - 4 March 2017 through 11 March 2017
ER -