View source for Synthesizing flight software (FSW) discrete controllers from formal specifications

{{righttoc}} 
This project is a collaboration with JPL to generate discrete controllers for flight software directly from formal specifications.

{| cellpadding=0 cellspacing=0 width=80%
|- valign=top
| 
Current participants:
{{project current participants}}
Additional participants:
{{project additional participants}}
|
Collaborators:
* Len Reder (JPL)

Past participants:
{{project past participants}}
|}

=== Objectives ===
[[Image:TuLiP-SCA.png|right|400px]]
The goal of this project is 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 its 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. 

=== References ===
{{project paper list}}

[[Category:Completed projects]]
<!-- [[Category:Subgroup projects]] -->
{{Project
|Title=Synthesizing flight software (FSW) discrete controllers from formal specifications
|Agency=JPL
|Grant number=IAMS100322
|Start date=1 Jan 2017
|End date=31 Dec 2017
|Support summary=Partial postdoc
|Reporting requirements=Final report
|Project ID=JPL CIF17
}}