The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - May-June (2013 vol.30)
pp: 50-57
Yannick Moy , AdaCore
Emmanuel Ledinot , Dassault-Aviation
Herve Delseny , Airbus
Benjamin Monate , TrustMySoft
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
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
REFERENCES
1. RTCA DO-178, “Software Considerations in Airborne Systems and Equipment Certification,” RTCA and EUROCAE, 2011.
2. NASA ARMD Research Opportunities in Aeronautics 2011 (ROA-2011), research program System-Wide Safety and Assurance Technologies Project (SSAT2), subtopic AFCS-1.3 Software Intensive Systems, p. 77; http://nspires.nasaprs.com/external/viewrepositorydocument/ cmdocumentid=320108/ solicitationId=%7B2344F7C4-8CF5-D17B-DB86-018B0B184C63%7D/ viewSolicitationDocument=1 ROA-2011%20Amendment%208%2002May12.pdf .
3. J. Rushby, “New Challenges in Certification for Aircraft Software,” Proc. 9th ACM Int'l Conf. Embedded Software, ACM, 2011; www.csl.sri.com/users/rushby/papersemsoft11.pdf .
4. RTCA DO-333, Formal Methods Supplement to DO-178C and DO-278A, RTCA and EUROCAE, 2011.
5. J. Souyris et al., “Formal Verification of Avionics Software Products,” Proc. Formal Methods, Springer, 2009; http://link.springer.com/chapter10.1007%2F978-3-642-05089-3_34?LI=true .
6. E. Ledinot and D. Pariente, “Formal Methods and Compliance to the DO-178C/ED-12C Standard in Aeronautics,” Static Analysis of Software, J.-L. Boulanger ed., John Wiley & Sons, 2012, pp. 207–272.
7. D. Brown et al., “Guidance for Using Formal Methods in a Certification Context,” Proc. Embedded Real-Time Systems and Software, 2010; www.open-do.org/wp-content/uploads/2013/ 03ERTS2010_0038_final.pdf.
8. P. Cuoq et al., “Frama-C, A Software Analysis Perspective,” Proc. Int'l Conf. Software Eng. and Formal Methods, Springer, 2012; www.springer.com/computer/swe/book978-3-642-33825-0 .
9. J. Barnes, SPARK, the Proven Approach to High Integrity Software, Altran Praxis, 2012.
10. J. Souyris and D. Favre-Félix, “Proof of Properties in Avionics,” Building the Information Society, IFIP Int'l Federation for Information Processing, René Jacquart, ed., vol. 156, 2004, pp. 527–535.
11. C. Comar, J. Kanig, and Y. Moy, “Integrating Formal Program Verification with Testing,” Proc. Embedded Real-Time Systems and Software, 2012; www.adacore.com/uploads_gemsHi-Lite_ERTS-2012.pdf .
63 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool