System and Component Software Specification, Run-time Verification and Automatic Test Generation, Phase I

The following background technology is described in Part 5: Run-time Verification (RV), White Box Automatic Test Generation (WBATG). Part 5 also describes how WBATG and RV yield Executable Model Checking (EMC). This proposal proposes using RV, WBATG and EMC for system level software verification. Similar techniques are commercially available for component level software (see Part 5 -- StateRover). The proposal suggests enhancing component-level UML-statechart visual modeling, code generation, Formal Specification of Correctness Properties (FS), RV, WBATG, and EMC towards the end of meeting the technology need of the subtopic, as follows: 1. Integrated specification-based and model-based WBATG for UML statechart models enhanced with FS. Having a seamless WBATG is required for system level verification because systems typically consist of a plurality of models and specifications making human driven verification difficult to perform. 2. Integrated white-box test generation of (1) with system level modeling using modeling. This integration will enable the use of system level data and models by the WBATG. 3. FS, RV, and WBATG's using the following system FS languages: Message Sequence Charts (MSC's) and Harel's Live Sequence Charts (LCS's). Items 1, 2 enable system level EMC as well as component-level EMC. Item 3 enables system level FS.

This is a mature technology (TRL 7+) — the realistic path in is usually NASA's Technology Transfer Program: licensing an existing NASA patent, or a Space Act Agreement to use NASA facilities/expertise directly. NASA also runs a startup licensing program with no upfront fee for companies formed to commercialize a specific NASA technology.

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.