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.