Combining Analyses for the Study of Numerical Invariants – CAFEIN

Activities were structured around three work-packages depending on their relative impact in the development cycle. The first one focuses on the collaboration of methods at model level (eg. synchronous languages) and the validation of properties after compilation into source code. The second work-package studies the more general setting in which the dynamic of the controlled object is concerned: the closed loop system with an hybrid semantics. Last, the third work-package focuses more specifically on numerical imprecision.

The first activity allowed us to propose new methods capable of automatically synthesizing invariants; for example using quantifier elimination or through the use of convex optimization. Methods have been proposed to enable the revalidation of proved properties along the development cycle.

Concerning hybrid systems, we proposed set-based simulation techniques using affine arithmetics and zonotopes. We also proposed SMT extension to support the description of hybrid systems and enabling the study of inductive properties over such systems.

Last, concerning numerical accuracy, more precise techniques such as the quadratic extension of affine arithmetics have been used to perform such analyses. Floating point aware methods have also been introduced in the compilation chain in order to increase the numerical accuracy of the final code.

The project identified numerous perspectives, for each task: new collaborations between methods in order to synthesize more expressive invariants, the extension of induction based reasoning to hybrid systems thanks to the hybrid extension of SMT solvers, and last the impact of considering floating point computation as early as possible in the development cycle.

42 papers including 19 in collaboration between partners, prototypes and a fruitful interaction with the twin US NSF CrAVES project.

This project addresses the formal verification of functional properties at specification level, for safety critical reactive systems. In particular, we focus on command and control systems interacting with a physical environment, specified using the synchronous language Lustre. Over the last 30 years, safety critical embedded software has known a steady exponential growth in both size and functional complexity. This increase of complexity is led by technical and safety requirements, but also to a large extent by economic requirements and environmental regulation. Furthermore, these systems are subject to hard certification constraints. The traditional process and test based approach to certification starts showing its limits, and formal methods, formal verification in particular, have emerged as a promising means of mastering this overwhelming complexity, both from the safety and from the economic point of view. The upcoming DO-178C acknowledges this evolution by recommending the use of model based techniques and formal verification techniques in the design, verification, validation and certification processes.

Despite the growing enthusiasm of industrial users, formal verification has not yet reached its full deployment potential. Costly human intervention is still needed in order to obtain expected results in real world applications. This project gathers a collective of experts in formal methods, hybrid systems modeling, tool providers and industrial partners, all active in the field of safety critical systems design, development and validation. The team will work on the design, implementation and evaluation of innovative cooperations of formal techniques, with the goal to increase the level of automation, scalability and robustness of formal verification at model level, widen its scope of application, and hopefully improve its economic
efficiency. Automatic generation of faithful implementations from models will also be addressed.

A first goal of the project is to improve the level of automation of formal verification, by adapting and combining existing verification techniques such as SMT-based temporal induction, and abstract interpretation for invariant discovery. Indeed, the complexity of formal verification is due to the superposition of two sources of complexity. First, the discrete and combinatorial control-flow, which in most of today's systems is based on the notion of clock (some portions of the computation are activated depending on logical conditions over the program's inputs or internal state). Second, the numerical complexity of the system's data-flow computation, which can in addition condition the activation of clocks, while being subject to non linear state invariants.

A second goal is to study how knowledge of the mathematical theory of hybrid command and control systems can help the analysis at the controller's specification level. The project will compute numerical invariants on control-command systems made of a synchronous controller (the Lustre program) and a Simulink description of the continuous environment. We will study how these invariants can be used both at the model level, in Lustre, as well as in the analysis of the generated software.


Third, the project addresses the issue of implementing real valued specifications in Lustre using floating point arithmetic. The difference in behavior between real and floats can introduce bugs that do not exist at specification level (overflows for example). Tools such as Fluctuat allow to evaluate formally this semantic distance. In this project, we propose to design code generation algorithms that are optimized for dealing with floating point issues. We will develop the tool Sardana in order to evaluate and minimize this semantic distance, and to some extent guarantee the preservation of properties already proved a specification level.