This tutorial is jointly organized by Aerospace Valley Formal Methods Forum and CGEE Working Group on comparison of safety standards. The objective of this tutorial is to present existing certification standards in different application domains (aeronautics, automotive, nuclear, railway, space) with a special focus on the verification means that are allowed/recommended/mandatory in these standards. Test has always been a classical verification means but formal methods are making their way into industrial practice and are handled differently by the certification standards. We propose a one- day tutorial, with the following program:
Tutorial room: Hourgade room, ADREAM building, LAAS
- 9h-10h: Overview of the place of formal methods in different safety standards — Jean-Paul Blanquart (CG2E Working Group)
- Even though most safety critical application domains and applicable safety standards share a largely common view on the acceptable means for development and safety assurance, there are also variations, which are important for instance for developers of applications or support tools in several domains, or even to support discussions towards evolution of standards. We will present a synthesis of similarities and differences between safety standards for what concerns the utilization of formal methods for certification (or qualification, acceptance...) and in particular with respect to "traditional" test-based justification. Addressed domains and standards will cover aeronautics (DO-178C), automotive (ISO 26262), industrial process automation (IEC 61508), nuclear (IEC 60880), railway (EN 50128) and space (ECSS-Q-ST-80C).
- 10h30-11h30: DO-178C Formal Methods Technical supplement — Virginie Wiels (Onera)
- DO-178 is the software certification standard for aeronautics. Version C of this standard has been published in 2011. It includes a specific supplement on the use of formal methods for software verification. This talk will present this supplement.
- 11h30-12h30: Industrial applications of formal methods in a certified context — Emmanuel Ledinot (Dassault Aviation) and Virginie Wiels (Onera)
- This talk will present two industrial applications of formal methods for software verification.
- 14h-15h30: Formal methods and railway — Jean-Louis Boulanger (CERTIFER)
- CENELEC EN 50128:2011 is the new standard for software development in the railway domain. In both versions of this standard (2001 and 2011) the use of formal methods is highly recommended. This recommendation is linked to the software safety integrity level (called SSIL). In this talk we present different examples of use of formal methods and we discuss their impact on the different verification activities. We also discuss the combination of proof and test to demonstrate software safety.
- 16h-17h: Panel — "Argumentation based on mixed formal/non formal evidence for the satisfaction of safety claims'' — animated by Gérard Ladier (Aerospace Valley) and Cyrille Comar (Adacore)
