Auto-Coding Flight Software Hybrid Controllers Synthesized from Formal Specifications

TBMG-26052

12/01/2016

Abstract
Content

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.

Meta TagsDetails
Citation
"Auto-Coding Flight Software Hybrid Controllers Synthesized from Formal Specifications," Mobility Engineering, December 1, 2016.
Additional Details
Publisher
Published
Dec 1, 2016
Product Code
TBMG-26052
Content Type
Magazine Article
Language
English