Hybrid theorem proving of aerospace systems: Applications and challenges

Complex software systems are becoming increasingly prevalent in aerospace applications: in particular, to
accomplish critical tasks. Ensuring the safety of these systems is crucial, as they can have subtly different behaviors
under slight variations in operating conditions. This paper advocates the use of formal verification techniques and in
particular theorem proving for hybrid software-intensive systems as a well-founded complementary approach to the
classical aerospace verification and validation techniques, such as testing or simulation. As an illustration of these
techniques, a novel lateral midair collision-avoidance maneuver is studied in an ideal setting, without accounting for
the uncertainties of the physical reality. The challenges that naturally arise when applying such technology to
industrial-scale applications is then detailed, and proposals are given on how to address these issues.