{"projectId":93889,"project":{"projectId":93889,"title":"Synthesizing Flight Software (FSW) Discrete Controllers from Formal Specifications","startDate":"2016-10-01","startYear":2016,"startMonth":10,"endDate":"2017-07-01","endYear":2017,"endMonth":7,"programId":164,"program":{"ableToSelect":false,"acronym":"JPL CIF","isActive":true,"description":"Through the Center Innovation Fund, the Space Technology Mission Directorate allocates a small portion of the NASA workforce and procurement budget to internal research and development to feed early stage innovation in technology and exploration. Activities with in the Center Innovation Fund are proposed and led by NASA scientists and engineers.  These activities and creative initiatives pursue emerging technologies that leverage talent and capabilities at the NASA Centers.    ","parentProgram":{"ableToSelect":false,"acronym":"CIF","isActive":true,"description":"<p>Through the Center Innovation Fund, the Space Technology Mission Directorate allocates a small portion of the NASA workforce and procurement budget to internal research and development to feed early stage innovation in technology and exploration.&nbsp;Activities with in the Center Innovation Fund are proposed and led by NASA scientists and engineers. &nbsp;These activities and creative initiatives pursue emerging technologies that leverage talent and capabilities at the NASA Centers.</p><p>&nbsp;</p><p>&nbsp;</p>","parentProgram":{"ableToSelect":false,"isActive":true,"description":"Catalyst is a portfolio of early stage programs that specialize in different innovation constituencies and mechanisms to push the state of the art in aerospace technology development","programId":92327,"responsibleMd":{"canUserEdit":false,"locationEdit":false,"organizationRolePretty":"","organizationTypePretty":""},"title":"Catalyst","manageGaps":false,"acronymOrTitle":"Catalyst"},"parentProgramId":92327,"programId":64,"responsibleMd":{"canUserEdit":false,"locationEdit":false,"organizationRolePretty":"","organizationTypePretty":""},"stockImageFileId":36643,"title":"Center Innovation Fund","manageGaps":false,"acronymOrTitle":"CIF"},"parentProgramId":64,"programId":164,"responsibleMd":{"organizationId":4875,"organizationName":"Space Technology Mission Directorate","acronym":"STMD","organizationType":"NASA_Mission_Directorate","canUserEdit":false,"locationEdit":false,"organizationRolePretty":"","organizationTypePretty":"NASA Mission Directorate"},"responsibleMdOffice":4875,"stockImageFileId":36651,"title":"Center Innovation Fund: JPL CIF","manageGaps":false,"acronymOrTitle":"JPL CIF"},"description":"<p>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></p>","benefits":"<p>To improve and optimize the use of combined control synthesis algorithms and code generation techniques to produce FSW directly from formal specifications.</p>","releaseStatus":"Released","status":"Completed","viewCount":586,"destinationType":[],"trlBegin":1,"trlCurrent":3,"trlEnd":3,"lastUpdated":"12/18/25","favorited":false,"detailedFunding":false,"projectContacts":[{"contactId":290429,"canUserEdit":false,"firstName":"Leonard","lastName":"Reder","fullName":"Leonard J Reder","fullNameInverted":"Reder, Leonard J","middleInitial":"J","email":"leonard.j.reder@jpl.nasa.gov","receiveEmail":"Subscribed_User","projectContactRole":"Principal_Investigator","projectContactId":548092,"projectId":93889,"programContactRolePretty":"","projectContactRolePretty":"Principal Investigator"}],"programContacts":[],"leadOrganization":{"organizationId":4946,"organizationName":"Jet Propulsion Laboratory","acronym":"JPL","organizationType":"FFRDC_2fUARC","city":"Pasadena","stateTerritoryId":59,"stateTerritory":{"abbreviation":"CA","country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"name":"California","stateTerritoryId":59,"isTerritory":false},"country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"zipCode":"91109","projectId":93889,"projectOrganizationId":575833,"organizationRole":"Lead_Organization","canUserEdit":false,"locationEdit":false,"organizationRolePretty":"Lead Organization","organizationTypePretty":"FFRDC/UARC"},"otherOrganizations":[{"organizationId":4946,"organizationName":"Jet Propulsion Laboratory","acronym":"JPL","organizationType":"FFRDC_2fUARC","city":"Pasadena","stateTerritoryId":59,"stateTerritory":{"abbreviation":"CA","country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"name":"California","stateTerritoryId":59,"isTerritory":false},"country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"zipCode":"91109","projectId":93889,"projectOrganizationId":575833,"organizationRole":"Lead_Organization","canUserEdit":false,"locationEdit":false,"organizationRolePretty":"Lead Organization","organizationTypePretty":"FFRDC/UARC"},{"organizationId":3115,"organizationName":"California Institute of Technology","acronym":"CalTech","organizationType":"Academia","city":"Pasadena","stateTerritoryId":59,"stateTerritory":{"abbreviation":"CA","country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"name":"California","stateTerritoryId":59,"isTerritory":false},"country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"zipCode":"91125","murepUnitId":110404,"academicDegreeType":"Private_4_year","projectId":93889,"projectOrganizationId":575834,"organizationRole":"Supporting_Organization","canUserEdit":false,"locationEdit":false,"organizationRolePretty":"Supporting Organization","organizationTypePretty":"Academia"}],"primaryTx":{"taxonomyNodeId":11301,"taxonomyRootId":8817,"parentNodeId":11294,"code":"TX11.1.7","title":"Frameworks, Languages, Tools, and Standards","description":"A common set of frameworks, languages, tools, and standards enable the management of both short- and long-term complexity in sharing, exchanging, and integrating software solutions from diverse sources. These technologies will reduce the costs associated with software development.","exampleTechnologies":"Reusable software libraries, common simulation frameworks, common ground system architectures, common communication protocols, common standards for trajectory parameterization/models, common command and data handling architectures","level":3,"hasChildren":false,"selected":false,"isPrimary":true,"hasInteriorContent":true},"primaryTxTree":[[{"taxonomyNodeId":11293,"taxonomyRootId":8817,"code":"TX11","title":"Software, Modeling, Simulation, and Information Processing","level":1,"hasChildren":true,"selected":false,"hasInteriorContent":true},{"taxonomyNodeId":11294,"taxonomyRootId":8817,"parentNodeId":11293,"code":"TX11.1","title":"Software Development, Engineering, and Integrity","description":"This area covers technologies for the design, development, testing, and verification of software systems.","level":2,"hasChildren":true,"selected":false,"hasInteriorContent":true},{"taxonomyNodeId":11301,"taxonomyRootId":8817,"parentNodeId":11294,"code":"TX11.1.7","title":"Frameworks, Languages, Tools, and Standards","description":"A common set of frameworks, languages, tools, and standards enable the management of both short- and long-term complexity in sharing, exchanging, and integrating software solutions from diverse sources. These technologies will reduce the costs associated with software development.","exampleTechnologies":"Reusable software libraries, common simulation frameworks, common ground system architectures, common communication protocols, common standards for trajectory parameterization/models, common command and data handling architectures","level":3,"hasChildren":false,"selected":true,"hasInteriorContent":true}]],"technologyOutcomes":[],"libraryItems":[],"states":[{"abbreviation":"CA","country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"name":"California","stateTerritoryId":59,"isTerritory":false}],"endDateString":"Jul 2017","startDateString":"Oct 2016"}}