Ebook: Static Analysis of Software: the Abstract Interpretation

Cover -- Title Page -- Copyright Page -- Table of Contents -- Introduction -- Chapter 1. Formal Techniques for Verification and Validation -- 1.1. Introduction -- 1.2. Realization of a software application -- 1.3. Characteristics of a software application -- 1.4. Realization cycle -- 1.4.1. Cycle in V and other realization cycles -- 1.4.2. Quality control (the impact of ISO standard 9001) -- 1.4.3. Verification and validation -- 1.5. Techniques, methods and practices -- 1.5.1. Static verification -- 1.5.2. Dynamic verification -- 1.5.3. Validation -- 1.6. New issues with verification and validation -- 1.7. Conclusion -- 1.8. Bibliography -- Chapter 2. Airbus: Formal Verification in Avionics -- 2.1. Industrial context -- 2.1.1. Avionic systems -- 2.1.2. A few examples -- 2.1.3. Regulatory framework -- 2.1.4. Avionic functions -- 2.1.5. Development of avionics levels -- 2.2. Two methods for formal verification -- 2.2.1. General principle of program proof -- 2.2.2. Static analysis by abstract interpretation -- 2.2.3. Program proof by calculation of the weakest precondition -- 2.3. Four formal verification tools -- 2.3.1. Caveat -- 2.3.2. Proof of the absence of run-time errors: Astrée -- 2.3.3. Stability and numerical precision: Fluctuat -- 2.3.4. Calculation of the worst case execution time: aiT (AbsInt GmbH) -- 2.4. Examples of industrial use -- 2.4.1. Unitary proof (verification of low level requirements) -- 2.4.2. The calculation of worst case execution time -- 2.4.3. Proof of the absence of run-time errors -- 2.5. Bibliography -- Chapter 3. Polyspace -- 3.1. Overview -- 3.2. Introduction to software quality and verification procedures -- 3.3. Static analysis -- 3.4. Dynamic tests -- 3.5. Abstract interpretation -- 3.6. Code verification -- 3.7. Robustness verification or contextual verification -- 3.7.1. Robustness verifications.;The existing literature currently available to students and researchers is very general, covering only the formal techniques of static analysis. This book presents real examples of the formal techniques called "abstract interpretation" currently being used in various industrial fields: railway, aeronautics, space, automotive, etc. The purpose of this book is to present students and researchers, in a single book, with the wealth of experience of people who are intrinsically involved in the realization and evaluation of software-based safety critical systems. As the authors are people currently working within the industry, the usual problems of confidentiality, which can occur with other books, is not an issue and so makes it possible to supply new useful information (photos, architectural plans, real examples).