P. Cousot, Avionic Software Verification by Abstract Interpretation.

Patrick Cousot.
Avionic Software Verification by Abstract Interpretation.
2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation. Special Workshop Theme: Formal Methods in Avionics, Space and Transport , Poitiers, France, December 12—14 2007.

Abstract:
A flight control surface actuation system in avionics is safety critical and complex since it is placed between the pilot's controls (sidesticks, rudder pedals) and the control surfaces of the aircraft, whose movement it controls and monitors. For reliability and dependability, several redundant software and computers are used but each one must be proved to be correct. With the exponential increase of the power of computers, the flight control software has become much more powerful hence complex. Since the cost of tests is increasing more rapidly that the size of programs, formal methods become an attractive complement for program verification.
The difficulties with formal methods are that they need a formal specification, a formal semantics of the programming language and, because of undecidability, have serious limits in the automatic verification that the program semantics satisfies the specification. A theorem prover needs human assistance while model-checking requires finite models which, but for hardware components, are generally incomplete.
Static analysis offers an interesting completely automatic alternative in that the specification can be chosen to be implicit. For example the absence of runtime error will not require the user to define a complex specification. Moreover static analysis considers infinite models of computations that can be directly computed from the program text so that the end-user does not need to provide a (finite) model of the program computations and environment. Finally, the reachable states during any program computation are computed approximately through an overapproximation that omits no possible case. So the delicate questions about the program semantics can be solved by considering all possible alternatives.
If this overapproximation copes with the undecidability problem, its inconvenience is that it considers spurious program behaviors, which do not exist in any actual execution, but may be at the origin of alarms, so-called “false alarms”. This approach is sound in that no runtime error will ever be omitted in the diagnostic. It is incomplete, because of the potential false alarms. In general false alarms have to be solved by manual code inspection, which is extremely costly.
The whole problem is therefore to choose abstractions of the program semantics that yield few or no alarm. To do so, one can restrict the family of programs to be analyzed so as to adapt the abstraction exactly the domain-specific primitives and algorithmic schema found in this family of programs.
We will present elements of the theory of abstract interpretation on which the soundness of the notion of overapproximation does rely. Then we will introduce the ASTRÉE static analyzer (www.astree.ens.fr), which is specialized for the verification of the absence of runtime errors in control-command programs. The analyzer has general-purpose abstractions (e.g. octagons, control and data partitioning) as well as domain-specific abstractions (e.g. to handle filters or the potential accumulation of rounding errors). Finally, we will report on the successful application of ASTRÉE to the proof of absence of runtime errors in recent avionic flight control software.

The slides of the 60mn talk are available in PDF format, 4 slides per A4 landscape page, to be used Acrobat Reader
- pdf (2 Mb)

Bibliographic reference:

\bibitem{Cousot-ISOLA07}
P.~Cousot.
\newblock Avionic Software Verification by Abstract Interpretation.
\newblock \emph{2007 ISoLA Workshop On Leveraging Applications of Formal 
          Methods, Verification and Validation. Special Workshop Theme: 
          Formal Methods in Avionics, Space and Transport}, 
          Poitiers, France, December 12--14 2007.

@inProceedings{Cousot-ISOLA07,
   author =    {P{.} Cousot},
   title =     {Avionic Software Verification by Abstract Interpretation},
   booktitle = {2007 ISoLA Workshop On Leveraging Applications of Formal 
                Methods, Verification and Validation. Special Workshop Theme: 
                Formal Methods in Avionics, Space and Transport},
   address =   {Poitiers, France},
   month =     {December 12--14},
   year =      2007,
}

copyright notice
Last modified: Monday, 04-Jan-2010 13:50:06 CET