Formal Synthesis of Embedded Control Software: Application to Vehicle Management Systems

Motivated by the transition from federated to integrated architectures in aerial vehicles, we propose an automated methodology for the synthesis of correct-by-construction control protocols for vehicle management systems. We use linear temporal logic as the specification language for precisely describing correct behaviors of the system as well as the admissible dynamic behavior of the environment due to, for example, wind gusts and changes in the flight conditions. We apply the method in the context of dynamic power allocation among a number of subsystems of varying flight-criticality. The resulting power management protocol is guaranteed to be correct, with respect to the overall system specification, for all admissible environment profiles. This approach also enables reasoning about design tradeoffs such as between efficiency (imposed through formal specifications) and system weight (characterized by the amount of required power generation and energy storage). We present our preliminary results in a simple setting and discuss extensions of the methodology to capture more realistic system and environment models and specifications.