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.
CEA LIST CEA LIST
ANR grant: 809 839 euros
Project ID: ANR-12-INSE-0007
Monsieur Pierre-loic Garoche (ONERA DTIM)
The project coordinator is the author of this abstract and is therefore responsible for the content of the summary. The ANR disclaims all responsibility in connection with its content.