NASA Logo, National Aeronautics and Space Administration

+NASA Home

+Ames Home

Robust Software Engineering Completes System-Wide Safety Application Programming Interface Milestone
Intelligent Systems Division Banner

Robust Software Engineering Completes System-Wide Safety Application Programming Interface Milestone

The Robust Software Engineering (RSE) group has completed the System-Wide Safety (SWS) Application Programming Interface (API) milestone for Assurance of Autonomy:

API 20 TC4 3.2.5.1 Demonstration of formalized requirements being tracked through design and code, and test cases generated from formalized requirements

RSE met this milestone with the development and demonstration of the integration of the Formalized Requirement Elicitation Toolset (FRET) tool with the Contract-based Compositional verification of SIMulink models (CoCoSim) tool, which performs model checking of formal safety properties on Simulink models.

BACKGROUND: FRET is used to generate formal properties, which can be used in formal verification in the later stages of the development process, in this case, in the design stage. With the help of FRET, safety requirements are formalized to create formal safety properties that are checked against Simulink models by CoCoSim. Since the demonstration is with CoCoSim, safety requirements are automatically translated to Simulink observers, which are then used by CoCoSim to verify the safety of Simulink models of the target system. (Note that FRET can also formalize requirements into other formal languages, e.g., future and past linear temporal logic; and that it also performs checks between requirements, e.g., consistency).

Automatic test case generation is also possible through the automatic test case generation capabilities of CoCoSim; thus requirement-based test generation can be achieved by using CoCoSim capabilities on the Simulink observers created by FRET. This combination of FRET and CoCoSim has been demonstrated using the formal verification challenges from Lockheed Martin. The work was presented at the “26th Working Conference on Requirement Engineering: Foundation for Software Quality” (RESQF 2020) in June 2020, and at the Requirements Engineering Conference (RE 2020) August 31-September 4.

This work has also been presented to the GE Global Research Center, GE Aviation, and Boeing. GE is demonstrating how formal observers can be generated by FRET and used for runtime monitoring during operations; such observers are guaranteed to provide assurance according to requirements. Boeing is planning to use FRET in the context of their demonstration of advanced Verification and Validation (V&V) techniques in December 2020.

NASA PROGRAM FUNDING: System-Wide Safety (SWS) project, Airspace Operations and Safety Program (AOSP), Aeronautics Research Mission Directorate (ARMD)

TEAM: Hamza Bourbouh, Pierre-Loic Garoche, Dimitra Giannakopoulou, Mohammad Hejase, Anastasia Mavridou, Thomas Pressburger, and Johann Schumann

POINT OF CONTACTS: Guillaume Brat, guillaume.p.brat@nasa.gov; and Dimitra Giannakopoulou, Dimitra.giannakopoulou@nasa.gov

First Gov logo
NASA Logo - nasa.gov