Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Computer Laboratory
Computer Laboratory > Abstracts

Seminars will be held in the Lecture Theatre 1 - William Gates Building, Computer Laboratory at 4.15pm
See also:

 Networks & OS seminars
 Security seminars
 Logic and Semantics seminars
 weekly timetable
for other seminars

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, 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

Wednesday Seminars

Click here for previous seminars.