This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Testing or Formal Verification: DO-178C Alternatives and Industrial Experience
May-June 2013 (vol. 30 no. 3)
pp. 50-57
Yannick Moy, AdaCore
Emmanuel Ledinot, Dassault-Aviation
Herve Delseny, Airbus
Benjamin Monate, TrustMySoft
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:
Yannick Moy, Emmanuel Ledinot, Herve Delseny, Virginie Wiels, Benjamin Monate, "Testing or Formal Verification: DO-178C Alternatives and Industrial Experience," IEEE Software, vol. 30, no. 3, pp. 50-57, May-June 2013, doi:10.1109/MS.2013.43
Usage of this product signifies your acceptance of the Terms of Use.