SURF 2017: Synthesizing flight software (FSW) discrete controllers from formal specifications

From Murray Wiki
Jump to navigationJump to search

2017 SURF: project description

  • Mentor: Richard M. Murray
  • Co-mentor: TBD

The Temporal Logic Planning (TuLiP) toolbox is a Python-based package for synthesizing reactive control protocols. It provides construction of a state machine that ensures a given formal specification is met (i.e., it is correct-by-construction). JPL has developed the StateChart Autocoder (SCA) generates state machine implementations from UML suitable for FSW deployment on JPL projects. Recent projects have developed an interface between TuLiP and SCA for feasibility demonstrations.

In this research we will improve TuLiP/SCA hybrid controller synthesis techniques for potential flight project use. The current state of the art produces designs that are not optimal: states and transitions are not minimized, and hierarchy to simplify designs has not been introduced. Optimization of the synthesized hybrid-controller design that is generated by TuLiP will be performed at Caltech. Caltech will explore and implement new algorithms to minimize the number of states produced in a TuLiP generated controller design – potentially incorporating generation of hierarchical state-machines. Currently the formal specifications (i.e. LTL, system dynamics, and constraints) that are input into TuLiP are daunting, intricate, and difficult to use for specifying a complex system and not suitable for the typical FSW or controls engineer to utilize. A Domain Specific Language (DSL) will be developed to improve and tailor the input specification sematic and make it easier for the FSW development engineer to use. To define the DSL, JPL will leverage it’s MSL and ISF (Instrument Software Framework) experiences along with the Caltech experience of already developing a DSL for aircraft power system controller synthesis. Finally state space explosion results in large numbers of states executing in TuLiP/SCA synthesized controllers and methods to limit state space explosion will be exercised. JPL will utilize the new refined technology, with Caltech support, to produce a proof-of-concept demonstration controller example thereby maturing the technology and preparing it for use on an actual flight project.

This SURF project will assist in the expansion and demonstration of TuLiP for synthesize flight software. Students interested in this project should have good programming skills, be familiar with Python, and have some background in either automata theory or control theory.

References

  1. Temporal Logic Planning Toolbox (TuLiP) available http://tulip-control.org
  2. JPL StateChart Autocoder (SCA) available https://github.com/JPLOpenSource/SCA
Retrieved from "https://murray.cds.caltech.edu/index.php?title=SURF_2017:_Synthesizing_flight_software_(FSW)_discrete_controllers_from_formal_specifications&oldid=21091"