The Community for Technology Leaders
Green Image
Issue No. 03 - May-June (2013 vol. 30)
ISSN: 0740-7459
pp: 50-57
Benjamin Monate , TrustMySoft
Emmanuel Ledinot , Dassault-Aviation
Herve Delseny , Airbus
Yannick Moy , AdaCore
ABSTRACT
Software for commercial aircraft is subject to the stringent certification processes described in the DO-178B standard, "Software Considerations in Airborne Systems and Equipment Certification." Issued in 1992, this document focuses strongly on the verification process, with a major emphasis on testing. In 2005, the avionics industry initiated an effort to update DO-178B, in large part to accommodate development practices (including formal verification techniques) that had matured since its publication. A revised standard, DO-178C, was issued in late 2011, incorporating new guidance that allows formal verification to replace certain forms of testing. In this article, the authors describe some of the new objectives and activities in the area of formal methods, explain how these methods may be used instead of testing in a DO-178C context, and summarize the practical experience of Dassault-Aviation and Airbus in successfully applying the new DO-178C approach. The first Web extra at http://youtu.be/tRtK4xOK-8o is part 1 of a video talk by Hervé Delseny, describing Airbus's use of formal methods to verify avionics software and summarizing the integration of formal methods in the upcoming ED-12/DO-178 issue C. The second Web extra at http://youtu.be/BVI5J1GAQ30 is part 2 of a video talk by Hervé Delseny, describing Airbus's use of formal methods to verify avionics software and summarizing the integration of formal methods in the upcoming ED-12/DO-178 issue C. The third Web extra at http://youtu.be/U3G1ZOoqg78 is part 3 of a video talk by Hervé Delseny, describing Airbus's use of formal methods to verify avionics software and summarizing the integration of formal methods in the upcoming ED-12/DO-178 issue C. The fourth Web extra at http://youtu.be/WtlqS-JOHrA is part 4 of a video talk by Hervé Delseny, describing Airbus's use of formal methods to verify avionics software and summarizing the integration of formal methods in the upcoming ED-12/DO-178 issue C.
INDEX TERMS
Software reliability, Formal verification, Aerospace electronics, Air transportation, Electronic mail, Facsimile, Testing, Software testing, Certification, DO-178, certification, formal methods, avionics software
CITATION
Benjamin Monate, Emmanuel Ledinot, Herve Delseny, Virginie Wiels, Yannick Moy, "Testing or Formal Verification: DO-178C Alternatives and Industrial Experience", IEEE Software, vol. 30, no. , pp. 50-57, May-June 2013, doi:10.1109/MS.2013.43
179 ms
(Ver )