Automatic Verification of Avionic Synchronous Safety Critical Embedded
Software
Patrick Cousot
Ecole normale superieure, Paris
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è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.
You can view the seminar slides from CousotCAMseminar04_4-1.pdf
