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.

Currently in projects at JPL, human engineers receive a list of requirements that must be achieved by the final product. As part of the design process — and consistent with so-called model-based software engineering — UML Statecharts are manually constructed (in MagicDraw) to capture the discrete-event interactions of the various components that will later have concrete implementations. The process involves interpretation of informal system requirements and the manual translation into UML. While the technique has been used for over a decade and significantly reduces development time, improves robustness, and increases maintainability, the design of state machines is known to be subtle and error-prone. Logical bugs are sometimes introduced in the manually designed Statecharts due to poor translation of requirements. SCA generates FSW implementations in C/C++, Python (for desktop functional simulation), or Promela (for functional design verification); however, the implementation generated is not complete in the sense that an engineer must still provide manually developed implementations for the various routines invoked during execution of a Statechart, e.g., evaluating guards and taking actions on transitions, and performing the entry and exit methods for each state.

This work demonstrates that the traditional steps of requirements, design, and implementation can effectively be reduced to formal requirements specification followed by the automated generation of a complete FSW implementation, thereby circumventing the error-prone and costly manual design and coding phases. Risk of latent design errors and testing time are both reduced.

Recent hybrid control systems research has produced algorithms that can automatically synthesize finite state machine (FSM) representations from formal specifications (or requirements), thus guaranteeing correct functionality (i.e., correct-by-construction), and potentially replacing the UML Statechart design process used today. TuLiP provides methods for state-machine synthesis from linear temporal logic (LTL) specifications, along with routines for control input computation for several classes of dynamical systems, e.g., linear time-invariant with disturbances.

An interface between TuLiP and SCA provides the capabilities described previously. Implementation code for two proof-of-concept controller examples was fully synthesized from formal specifications — no code was manually developed. The process of embedded FSW development at JPL could be dramatically streamlined (e. g. verification and validation efforts reduced) with maturity of this research.

The software provides additional capability within TuLiP Python software to generate UML Statecharts as XMI files, and generate implementation codes for Statechart action functions allowing continuous dynamics updates. The software interfaces TuLiP and JPL Statechart Autocoder Rev. 2 for implementation of flight controllers.

This work was done by Leonard J. Reder, Scott C. Livingston, Sumanth Dathathri, and Richard Murray of Caltech for NASA’s Jet Propulsion Laboratory. This software is available for license through the Jet Propulsion Laboratory, and you may request a license at: NPO-49953