Static Analysis of Control Command Systems:
Synthesizing non Linear Invariants

Keywords: abstract interpretation, control command systems, quadratic invariants, policy iteration, ellipsoids, semi-definite programming

Summary: Digital flight commands are now widespread in large commercial aircrafts. These control command systems are said critical in the sense that a failure could have serious impacts, particularly in terms of human lives, hence their stringent validation demands and a strong interest in formal proofs of correctness.

In 1987, the Airbus A320 performed its first flight, being the first commercial aircraft with digital flight commands. Boeing followed the same path less than ten years later with the maiden flight of its B777 in 1994 and nowadays the design of a large commercial aircraft cannot be envisioned anymore without digital flight commands. They even begin to be introduced in business jets and helicopters.

Electrical flight commands allow inherently unstable aircraft designs which a human being would otherwise be unable to pilot. In the field of combat aircrafts, this gave birth to planes with incredible maneuverability, while relaxing the stability of commercial aircrafts allows to reduce the size of the control surfaces, decreasing both their weight and drag which leads to improved fuel efficiency.

Digital flight commands allow to add new features among which the most iconic is probably the flight envelope protection. This system prevents the aircraft from being put in dangerous postures whatever the pilot do with its stick. In particular, this allows them to react quickly in an emergency situation without having to take care not to exceed the structural or aerodynamic limits of their aircraft.

Critical Systems such as flight commands may have disastrous results in case of failure. Therefore, they have to meet stringent certification requirements. This is currently enforced by means of extensive testing. This can be considered successful in the sense that after decades of daily operations of thousands of aircrafts no loss of life can be imputed to a software failure in a numerical flight command system. Such process are nonetheless terribly heavy and expensive. Furthermore, the number of cases to test being way too large, exhaustive testing is intractable and there is no guarantee that the chosen test cases do not fail to expose a bug. All this explains the interest of both the industrial and the academic communities in formal methods able to more or less automatically deliver mathematical proof of correctness. Among them, this thesis will particularly focus on abstract interpretation, an efficient method to automatically generate proofs of numerical properties which are essential in our context.

It is well known from control theorists that linear controllers are stable if and only if they admit a quadratic invariant (geometrically speaking, an ellipsoid). They call these invariants quadratic Lyapunov functions and a first part offers to automatically compute such invariants for controllers given as a pair of matrices. This is done using semi-definite programming optimization tools. It is worth noting that floating point aspects are taken care of, whether they affect computations performed by the analyzed program or by the tools used for the analysis.

However, the actual goal is to analyze programs implementing controllers (and not pairs of matrices), potentially including resets or saturations, hence not purely linears. The policy iteration technique is a recently developed static analysis techniques well suited to that purpose. However, it does not marry very easily with the classic abstract interpretation paradigm. The next part tries to offer a nice interface between the two worlds.

Finally, the last part is a more prospective work on the use of polynomial global optimization based on Bernstein polynomials to compute polynomial invariants on polynomials systems.