Static Analysis of Software: The Abstract Interpretation

by Jean-Louis Boulanger (Editor)

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 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).

Contents

Introduction

1. Formal techniques for verification and validation (Jean-Louis Boulanger)

2. Airbus: Formal verification in avionics (Jean Sourys, David Delmas, Stéphane Duprat)

3. Polyspace (Patrick Munier)

4. Software robustness with regards to dysfunctional values from static analysis (Christèle Fauré, Jean-Louis Boulanger, Samy Aït Kaci)

5. CodePeer – Beyond bug-finding with static analysis (Steve Baird, Arnaud Charlet, Yannick Moy, Tucker Taft)

6. Formal methods and compliance to the DO-178C/ED-12C Standard in Aeronautics (Emmanuel Ledinot, Dillon Pariente)

7. Efficient method developed by Thales for safety evaluation of real-to-integer discretization and overflows in SIL4 (Anthony Baëotto, Fateh KaakaË, Rafael Marcano, Daniel Drago)

8. Conclusion and viewpoints (Jean-Louis Boulanger)

331 pages, Hardcover

First published December 12, 2011

Reviews

[Alejandro Teruel · Rating 3 out of 5]

In his conclusions in chapter 8, the editor and co-author of several chapters, Jean-Louis Boulanger states that

This book is part of a series of four books that cover different aspects of formal techniques: static analysis of code; B method; and formal methods.

[This] first volume concerns industrial examples of the implementation of formal techniques based on static analysis, such as the abstract interpretation and proof of programs to develop certifiable software applications in avionics, automobile, nuclear powerstation and railway control systems. There are examples of use of Astrée tools (chapter 2), Caveat (chapter 2), CodePeer (chapter 5), Frama-C (Chapters 2 and 6), Polyspace (Chapters 3 and 4) and Scade, as well as an example of generated C code analysis (Chapter 7). In these chapters the static code analyses are based on:

- Abstract interpretation as based on the pioneering work of Patrick and Radhia Cousot (chapters 2, 3, 4, and 6);

- Program proof as based on Hoare axiomatics (chapters 2, 5 and 6);

- Static analysis of code (chapters 2, 5, 6 and 7)

He also expresses that:

It is worth noting that the abstract interpretation tools such as Polyspace or Astrée are not new but their efficiency has evolved a great deal. We have moved on from tools tthat, 15 years ago, could require a week's worth of calculations to analyze a code, to trools that require only tens of minutes to arrive at results.

This is not an easy book to read and requires a great deal of knowledge about formal methods, automatic software code provers, interval artithmetic and especially abstract interpretation. According to Wikipedia:

...Abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics (e.g., control-flow, data-flow) without performing all the calculations.

Tools based on abstract interpretation can be used to determine, without dynamically executing the code being examined, whether it contains dead (unreachable) code, divisions by zero, arithmetic overflows or underflows, out of bounds array indexes, uninitialized variables, other execution time anomalies and certain safety and liveliness properties. The use of such tools are particularly interesting and important in safety-critical applications.

I confess that most of the book was beyond me, even though I have some knowledge of Hoare axiomatics, fixed point theory, floating-point representations, safety critical properties and have worked with formal specification languages. However I have next to no knowledge of static analysis and had no previous knowledge of abstract interpretation. I skimmed through this book and was pleasantly surprised by the state of the art, static analysis tools and techniques had reached by 2011 when the book was published, especially by their industrial use in the development of certified safety-critical software ranging from tens of thousands of lines of code to five hundred thousand lines of code. The book certainly left me intrigued by its subject matter. My three-star evaluation of the book should be taken with at least a bucketful of salt; to be fair, the book should really be evaluated by a far more knowledgeable reader in the subject area.