P. Cousot, Automatic Verification of Avionic Synchronous Safety Critical Embedded Software

Patrick Cousot.
Automatic Verification of Avionic Synchronous Safety Critical Embedded Software.
Programming Languages Seminar, College of Computer and Information Science, Northeastern University, Boston, Massachusetts, USA. June 1^st, 2005.
Abstract:
   A basic property of software is that there should be no reachable state of the computations in which an undefined operation can be performed. For example in synchronous software, as found in safety critical embedded application such as electric flight control, a runtime error might raise an interrupt whence break the synchrony.
   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.
   An alternative is to use static analysis where an abstraction of the semantics of the programs is automatically computed which leaves out all information about reachable states which is not strictly necessary for the proof. Of course if the abstraction is too precise, the computation cost are too high (resourse exhaustion) and if it is too rough, nothing can be proved (false alarm). Although the best abstraction does exist, it is not computable, and so, must be found experimentally.
   We will provide an intuition for the underlying theory, that of abstract interpretation, and then report on an application to the proof of absence of runtime errors in the electric flight control system of commercial planes. In this project the abstraction has been tuned manually to get no false alarm, whence a correctness proof, certainly a world premi\`ere 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 30 mn presentation: The color transparencies are available as 1 slide per lanscape page for projection (1/1), 2 slides per portrait page for reading (2/1) and 4 slides per lanscape page for printing (4/1), in:
- PostScript: 1/1 .ps.gz, 2/1 .ps.gz, 4/1 .ps.gz for viewing with GhostScript and GhostView or (color) printing;
- PDF: 1/1 .pdf, 2/1 .pdf, 4/1 .pdf to be used with Acrobat Reader.

Bibliographic reference:

\bibitem{Cousot-NEU-01-06-05}
P.~Cousot.
\newblock Automatic Verification of Avionic Synchronous Safety
          Critical Embedded Software.
\newblock \emph{Programming Languages Seminar}, College of Computer 
          and Information Science, Northeastern University, Boston, 
          Massachusetts, USA. June 1st, 2005.

@conference{Cousot-NEU-01-06-05,
   author =    {P{.} Cousot},
   title =     {Automatic Verification of Avionic Synchronous Safety
                Critical Embedded Software},
   booktitle = {Programming Languages Seminar},
   address =   {College of Computer and Information Science, Northeastern
                University, Boston, Massachusetts, USA},
   month =     {1 June},
   year =      2005,
}

copyright notice, Springer copyright
Last modified: