• Patrick Cousot.
  Abstract-Interpretation-based Static Analysis of Safety-Critical Embedded Software.
  Airbus workshop on formal verification tools strategy, Toulouse, France. December 4^th, 2008.
• Abstract:
       Static software analysis has known brilliant successes in the small, by proving complex program properties of programs of a few dozen or hundreds of lines, either by systematic exploration of the state space or by interactive deductive methods. To scale up is a definite problem. Very few static analyzers are able to scale up to millions of lines without sacrificing automation and/or soundness and/or precision. Unsound static analysis may be useful for bug finding but is less useless in safety critical applications where the absence of bugs, at least of some categories of common bugs, should be formally verified.
       After recalling the basic principles of abstract interpretation including the notions of abstraction, approximation, soundness, completeness, false alarm, etc., we introduce the domain-specific static analyzer ASTR{\'E}E (\href{http://www.astree.ens.fr}{\texttt{www.astree.ens.fr}}) for proving the absence of runtime errors in safety critical real time embedded synchronous software in the large.
       The talk emphasizes soundness (no runtime error is ever omitted), parametrization (the ability to refine abstractions by options and analysis directives), extensibility (the easy incorporation of new abstractions to refine the approximation), precision (few or no false alarms for programs in the considered application domain) and scalability (the analyzer scales to millions of lines).
       In conclusion, present-day software engineering methodology, which is based on the control of the design, coding and testing processes should evolve in the near future, to incorporate a systematic control of final software product thanks to domain-specific analyzers that scale up.

• Keywords:
  Abstract Interpretation, Embedded software, Real-time software, Safety-critical software, Static analysis, Scalability, Software, Verification.
• Slides of the 55 mn presentation: .pdf (8.6 MB) to be read with Acrobat Reader.
-
• Bibliographic reference:

  \bibitem{Cousot-AIRBUS-2008-12-04}
  P.~Cousot.
  \newblock Abstract-Interpretation-based Static Analysis of Safety-Critical 
            Embedded Software.
  \newblock Airbus workshop on formal verification tools strategy, 
            Toulouse, France. December 4${^\mathrm{th}}$ 2008.
  
  @inProceedings{Cousot-AIRBUS-2008-12-04
     author =    {Cousot, P{.}},
     title =     {Abstract-Interpretation-based Static Analysis of Safety-Critical
                  Embedded Software},
     booktitle = {Airbus workshop on formal verification tools strategy},
     address =   {Toulouse, France},
     month =     {4 December},
     year =      {2008},
  }
  

Copyright notice
Last modified: Monday, 04-Jan-2010 11:37:57 CET