Aerospace Control Systems

Software has been an essential component of aerospace control since the earliest weather-satellite launches in the early 1960s. The complexity of aerospace software is growing rapidly, as key control features either migrate from human to computer control or are implemented directly within software to begin with. Within NASA in particular, we have observed near exponential growth of flight software in NASA missions in the past several decades, and the trend is likely to continue. Checking that the software controlling these applications works correctly, especially in the context of governmental regulations regarding safety, is an ongoing, costly, and time-consuming challenge.

The proposed research into MCAI will enable significant strides to be made in verifying aerospace control software. Abstract-interpretation-based techniques have been successfully applied to aircraft fly-by-wire control/command programs, mainly to verify safety properties, that is, to prove that the software does not “crash”. A challenge is to extend such techniques to liveness properties. For example, one would like to be able to automatically prove that, despite the failure of certain sensors and/or actuators, pressing the left rudder pedal will eventually move the rudder left to control yaw, perhaps within a given maximum time bound. This problem is much more difficult for systems of concurrent processes, since timings of asynchronous processes and interrupts are hard to predict. The innovations to be developed in this Expeditions project will lead to tools that address these issues.