A Caltech Library Service

Progress towards flight software hybrid controllers from formal specifications

Haesaert, S. and Reder, L. J. and Murray, R. M. (2018) Progress towards flight software hybrid controllers from formal specifications. In: 2018 IEEE Aerospace Conference. IEEE , Piscataway, NJ, pp. 1-17. ISBN 978-1-5386-2014-4.

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item:


The manual translation of informally defined requirements into statecharts, from which source code can be generated automatically, can be an error-prone, laborintensive process. Design errors sometimes propagate into final implementation code, only to be discovered during testing and verification. However, the requirements that the software needs to satisfy can be formally defined via temporal logics. In this paper, an approach to automatically synthesize flight-software hybrid-controllers for dynamic systems from formal specifications is given. First, specifications for a specific control functionality are defined by a set of linear temporal logic formulas. These, together with a model of the dynamical system, are then used as inputs to the Caltech-developed temporal logic planning toolbox (TuLiP), which searches for a control design. This results in a controller that is hybrid as it combines a finite state controller together with low-level continuous control actions. We map the resulting controller design to UML statecharts, which can be given as input to the Statechart Autocoder (SCA) developed by the Jet Propulsion Laboratory. SCA maps statechart controller designs to software implementation C code suitable for flight applications. By construction, the resulting code will meet the original formal design specifications, thus eliminating latent design errors. This paper describes the new 2nd generation interface developed to specify and convert the TuLiP-produced design to more optimized (e.g., reduced number of states and transitions) input UML (as XML file) for the JPL Statechart Autocoder. By applying intermediate optimization procedures, in which indistinguishable states are merged and transitions are grouped, the size of the statechart and the resulting code is reduced substantially. This is demonstrated by revisiting our 2016 speed-controller example showing reduction by more than 75% of the states synthesized in the original example.

Item Type:Book Section
Related URLs:
URLURL TypeDescription
Murray, R. M.0000-0002-5785-7481
Additional Information:© 2018 IEEE. This work was funded by a NASA, Space Technology Mission Directorate, Center Innovation Fund award granted to the Jet Propulsion Laboratory for purposes of investigating and improving the TuLiP and SCA capability to synthesize flight-like controllers from formal specifications. The authors wish to thank Rafi Some, the JPL Division 34 technologist, Dr. Andrew Shapiro and Dr. Tom Cwik of the JPL Technology office for support to perform this research.
Funding AgencyGrant Number
Record Number:CaltechAUTHORS:20180706-104554837
Persistent URL:
Official Citation:S. Haesaert, L. J. Reder and R. M. Murray, "Progress towards flight software hybrid controllers from formal specifications," 2018 IEEE Aerospace Conference, Big Sky, MT, USA, 2018, pp. 1-17. doi: 10.1109/AERO.2018.8396562
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:87593
Deposited By: George Porter
Deposited On:06 Jul 2018 20:27
Last Modified:03 Oct 2019 19:57

Repository Staff Only: item control page