P. Cousot & R. Cousot, Static Analysis of Embedded Control/Command Software by Abstract Interpretation

Patrick Cousot & Radhia Cousot.
Static Analysis of Embedded Control/Command Software by Abstract Interpretation.
Kestrel Technology, Palo Alto, California, November 7^th, 2005.
Abstract:
The talk briefly reviews abstract interpretation and its main applications. It then presents a practical application of abstract interpretation to the verification of safety critical embedded control-command software by the ASTRÉE static analyzer. It has been applied with success to the verification of absence of runtime errors in the control part of the primary flight control software of fly-by-wire systems of commercial planes. The state space of such huge programs (hundreds of thousands of lines) is so large that it cannot be explored explicitly by model-checking nor reasonably covered by testing. A (computer-aided) formal proof would be humanely insurmountable and economically very costly. The key to the verification by static analysis is the appropriate experimental choice of abstractions which can be tuned to yield no false alarm, certainly a world première for a program of that size (see the ASTRÉE project, http://www.astree.ens.fr/). We will conclude by grand challenges for static program/specification analysis the next 5 to 10 years.
Keywords:
Abstract Interpretation, Static Analysis, Embedded Systems, Control/Command Software, Reachability, Runtime Error, Verification.
Slides of the 60 mn presentation: .pdf.

Bibliographic reference:

\bibitem{Cousot-Kestrel-7-11-05}
P.~Cousot \& R. Cousot.
\newblock Static Analysis of Embedded Control/Command Software 
          by Abstract Interpretation.
\newblock Kestrel Technology, Palo Alto,, California, November 7, 2005.


@conference{Cousot-Kestrel-7-11-05,
   author =    {P{.} Cousot and R. Cousot},
   title =     {Static Analysis of Embedded Control/Command Software 
                by Abstract Interpretation},
   address =   {Kestrel Technology, Palo Alto,, California, USA},
   month =     {7 November},
   year =      2005,
}

copyright notice, Springer copyright
Last modified: Monday, 07-May-2012 17:51:02 EDT