Static Analysis of Software

Jean-Louis Boulanger is currently an Independent Safety Assessor (ISA) in the railway domain focusing on software elements. He is a specialist in the software engineering domain (requirement engineering, semi-formal and formal method, proof and model-checking). He also works as an expert for the French notified body CERTIFER in the field of certification of safety critical railway applications based on software (ERTMS, SCADA, automatic subway, etc.). His research interests include requirements, software verification and validation, traceability and RAMS with a special focus on SAFETY.

• Introduction xiJean-Louis BoulangerChapter 1. Formal Techniques for Verification and Validation 1Jean-Louis BOULANGER1.1. Introduction 11.2. Realization of a software application 11.3. Characteristics of a software application 31.4. Realization cycle 41.5. Techniques, methods and practices 131.6. New issues with verification and validation 391.7. Conclusion 411.8. Bibliography 42Chapter 2. Airbus: Formal Verification in Avionics 45Jean Souyris, David DELMAS and Stéphane DUPRAT2.1. Industrial context 452.2. Two methods for formal verification 522.3. Four formal verification tools 662.4. Examples of industrial use 802.6. Bibliography 109Chapter 3. Polyspace 113Patrick MUNIER3.1. Overview 1133.2. Introduction to software quality and verification procedures 1143.3. Static analysis 1163.4. Dynamic tests 1163.5. Abstract interpretation 1173.6. Code verification 1183.7. Robustness verification or contextual verification 1213.8. Examples of Polyspace® results 1233.9. Carrying out a code verification with Polyspace 1283.10. Use of Polyspace® can improve the quality of embedded software 1303.11. Carrying out certification with Polyspace® 1353.12. The creation of critical onboard software 1353.13. Concrete uses of Polyspace® 1353.14. Conclusion 1413.15. Bibliography 141Chapter 4. Software Robustness with Regards to Dysfunctional Values from StaticAnalysis 143Christèle FAURE, Jean-Louis BOULANGER and Samy AÏT KACI4.1. Introduction 1434.2. Normative context 1444.3. Elaboration of the proof of the robustness method 1464.4. General description of the method 1514.5. Computation of the control required 1574.6. Verification of the effective control of an industrial application 1614.7. Discussion and viewpoints 1724.8. Conclusion 1734.9. Bibliography 174Chapter 5. CodePeer – Beyond Bug-finding with Static Analysis 177Steve BAIRD, Arnaud CHARLET, Yannick MOY and Tucker TAFT5.1. Positioning of CodePeer 1775.2. A tour of CodePeer capabilities 1825.3. CodePeer’s inner working 1885.4. Conclusions 2045.5. Bibiliography 205Chapter 6. Formal Methods and Compliance to the DO-178C/ED-12C Standard in Aeronautics 207Emmanuel LEDINOT and Dillon PARIENTE6.1. Introduction 2076.2. Principles of the DO-178/ED-12 standard 2086.3. Verification process 2126.4. The formal methods technical supplement 2186.5. LLR verification by model-checking 2296.6. Contribution to the verification of robustness properties with Frama-C 2346.7. Static analysis and preservation of properties 2526.8. Conclusion and perspectives 2566.9. Appendices 2586.10. Acknowledgements 2686.11. Bibliography 269Chapter 7. Efficient Method Developed by Thales for Safety Evaluation of Real-to-Integer Discretization and Overflows in SIL4 Software 273Anthony BAÏOTTO, Fateh KAAKAÏ, Rafael MARCANO and Daniel DRAGO7.1. Introduction 2737.2. Discretization errors in the embedded code production chain 2747.3. Modeling of the creation and propagation of uncertainties 2807.4. Good practice of an analysis of real-to-integer discretization 2947.5. Arithmetic overflow and division by zero 2977.6. Application to a rail signalling example 2997.7. Conclusion 3077.8. Annexe: proof supplements 3087.9. Bibliography 317Conclusion and viewpoints 319Jean-Louis BOULANGERGlossary 323List of Authors 327Index 329