Static Analysis and Verification of Aerospace Software by Abstract Interpretation
Julien Bertrane
Niveau: Secondaire, Lycée, Première Static Analysis and Verification of Aerospace Software by Abstract Interpretation Julien Bertrane? Ecole normale superieure, Paris Patrick Cousot?,?? Courant Institute of Mathematical Sciences, NYU, New York & Ecole normale superieure, Paris Radhia Cousot? Ecole normale superieure & CNRS, Paris Jerome Feret? Ecole normale superieure & INRIA, Paris Laurent Mauborgne?,‡ Ecole normale superieure, Paris & IMDEA Software, Madrid Antoine Mine? Ecole normale superieure & CNRS, Paris Xavier Rival? Ecole normale superieure & INRIA, Paris We discuss the principles of static analysis by abstract interpretation and report on the automatic verification of the absence of runtime errors in large embedded aerospace software by static analysis based on abstract interpretation. The first industrial applications concerned synchronous control/command software in open loop. Recent advances consider imperfectly synchronous, parallel programs, and target code validation as well. Future research directions on abstract interpretation are also discussed in the context of aerospace software. Nomenclature S program states CJtKI collecting semantics FP prefix trace transformer F? interval transformer V set of all program variables t? reflexive transitive closure of relation t lfp?F least fixpoint of F for ? |x| absolute value of x q quaternion N naturals I initial states T JtKI trace semantics RJtKI reachability semantics 1S identity on S (also t0) x program variable tn powers of relation t ? abstraction function widening X] abstract counterpart of X q conjugate of quaternion q Z integers t state transition PJtKI prefix
- abstract interpretation
- s0 ?
- synchronous control
- program execution
- application domain
- formal verification
- software
- th state
- semantics can
- semantics