Synthesizing Flight Software (FSW) Discrete Controllers from Formal Specifications

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>

Data and Resources

Field Value
Groups
  • AmeriGEOSS
  • National Provider
  • North America
Tags
  • amerigeo
  • amerigeoss
  • ckan
  • geo
  • geoss
  • national
  • north-america
  • united-states
isopen False
license_id us-pd
license_title us-pd
maintainer TECHPORT SUPPORT
maintainer_email hq-techport@mail.nasa.gov
metadata_created 2025-12-02T07:08:31.551954
metadata_modified 2025-12-02T07:08:31.551958
notes 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>
num_resources 4
num_tags 8
title Synthesizing Flight Software (FSW) Discrete Controllers from Formal Specifications