Auto-Coding Flight Software Hybrid Controllers Synthesized from Formal Specifications

摘要

The technique of synthesizing state-machine-based hybrid controller flight software (FSW) from formal specifications is demonstrated utilizing two simple controller examples (i.e. a simple thermostat and a simple autonomous vehicle). Formal requirements for these controllers are specified using linear temporal logic (LTL) expressions, expressions describing the system dynamics, and numerical bounds on the control inputs and disturbances (or constraints). A new interface between the Temporal Logic Planning (TuLiP) toolbox - a hybrid controller synthesis software - and the JPL Statechart Autocoder (SCA) - a tool for mapping UML Statecharts to implementation code - was developed. The interface is still under development, but has reached sufficient maturity for demonstration. Results from preliminary prototype demonstrations encourage further collaboration between JPL and Caltech to develop a new capability for synthesizing hybrid controllers to be implemented within JPL Flight Software.