This thesis is proposed by ONERA's information processing and systems modelling department in Toulouse, France, in partneship with Rockwell
Collins France (French subsidiary of Rockwell Collins Inc.), a leading
designer and provider of critical aerospace systems, enjoying a
internationally renowned expertise in formal methods.
Critical systems and software are subject to diverse and drastic
requirements such as functional correctness under hard real-time
constraints, fault-tolerance constraints, reconfiguration constraints,
etc. Over the years, a range of model driven engineering techniques
and formal analysis methods and techniques were developed
(scheduling analysis, real-time performance prediction, automatic
bug finding, automatic proof of absence of bug, …) and refined to
reach a high maturity.
Despite these continuous advances in formal methods, users often
experience technical difficulties in scaling up formal methods to
models of real world systems, either because of their important size,
because or because of their inherent computational complexity (when
they make use of non linear integer arithmetic, or floating point
arithmetic for instance). Methodological and process issues can also
come in the way, but this thesis will be primarily focused on the
technical side of the problem.
Nevertheless, it seems some progress can be achieved on these
technical issues by establishing a tight cooperation between different
and mature approaches to formal verification.
In particular, SMT-based temporal model checking techniques (MC),
which allow to verify safety and liveness properties on transition
systems, have gained momentum thanks to the recent and dramatic
advances in SMT solvers performance, invariant strengthening for k-induction based techniques and Craig interpolant generation techniques for heterogeneous logics. Still,
proofs can fail, and extra non-trivial information (i.e. lemmas) often
has to be manually added to a model to allow a proof to be obtained.
Similarly, abstract interpretation (AI) techniques have become
extremely effective, but are somehow dedicated to the analysis of
predefined property patterns on imperative code, such as out of bounds
accesses in arrays, integer overflows/underflows, or to finding bounds
on the error between an ideal computation using real numbers and its
implementation using floating point numbers.
The Ph.D. student will have to study in which way these two families
of techniques (MC/AI) can complement each other so as to overcome
their own limitations, hopefully extending the range of critical
aerospace systems that can be addressed with formal methods.
Full details and contact information available in this
ONERA PDF document
The thesis will follow a CIFRE convention (Click for CIFRE financing information) | 
