← Back to NASA Technology Projects

Synthesizing Flight Software (FSW) Discrete Controllers from Formal Specifications

Completed TRL 3 (started at 1, targeting 3)

Description

This project will develop a Domain Specific Language (DSL) approach to interpret requirements and map them to formal specifications and legacy formats; explore and enhance the connection of TuLiP and SCA; develop methods to ensure semantics of the synthesized FSM designs map into implementations; and demonstrate the proof-of-concept synthesis on controller example cases. The key innovations will be: synthesis of FSM's that ensures a given formal specification is met (i.e., correct-by-construction). Also, complete software synthesis - no manually developed code>

Benefits

To improve and optimize the use of combined control synthesis algorithms and code generation techniques to produce FSW directly from formal specifications.

Details

Technology areaSoftware, Modeling, Simulation, and Information Processing > Software Development, Engineering, and Integrity > Frameworks, Languages, Tools, and Standards
ProgramCenter Innovation Fund: JPL CIF (JPL CIF)
Lead organizationJet Propulsion Laboratory, Pasadena, CA
Start date2016-10-01
End date2017-07-01

Project contacts

Listed on TechPort itself — the most direct way to ask about this specific project.

How to get involved

This is early/mid-stage (TRL 3) — the most realistic path in is NASA SBIR/STTR, which funds small businesses and research institutions to develop technology aligned with NASA's needs (equity-free, phased funding). Check whether a current SBIR/STTR solicitation topic overlaps with this project's technology area, or contact the project directly (above) to ask.

None of these are guaranteed paths for this specific project — TechPort itself doesn't have an "apply" button. Reaching out to the contact(s) above with a specific question is usually the fastest way to find out what's actually open.