Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published March 2018 | public
Book Section - Chapter

Progress towards flight software hybrid controllers from formal specifications

Abstract

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.

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.

Additional details

Created:
August 19, 2023
Modified:
October 18, 2023