NASA SBIR 2005 Solicitation

FORM B - PROPOSAL SUMMARY


PROPOSAL NUMBER:05 X5.01-9960
SUBTOPIC TITLE:Software Engineering
PROPOSAL TITLE:System and Component Software Specification, Run-time Verification and Automatic Test Generation

SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
Time Rover
11425 Charsan Lane
Cupertino ,CA 95014 - 4981
(408) 252 - 2808

PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
Doron   Drusinsky
nasa_sbir@time-rover.com
11425 Charsan Lane
Cupertino, CA  95014 -4981
(408) 252 - 2808

TECHNICAL ABSTRACT (LIMIT 200 WORDS)
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.

POTENTIAL NASA COMMERCIAL APPLICATIONS (LIMIT 150 WORDS)
NASA/JPL relies heavily on Matlab for system modeling. On the other hand, existing tools and techniques for robust and scalable software verification work primarily on the component level. Robust system level verification will provide significant improvement to the level of NASA's system and software safety because real-environment models will be usable in conjunction with robust formal methods.

POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (LIMIT 150 WORDS)
NASA/JPL relies heavily on Matlab for system modeling. On the other hand, NASA's formal method and run-time verification efforts have been using on temporal logic and some statechart specifications for run-time verification model checking. Integrating these two aspects of system representation will provide significant improvement to the level of NASA's system and software safety because real-environment models will be usable in conjunction with robust formal methods. This is the positioning of our commercialization strategy within NASA.
Time Rover's UML-statechart based modeling, specification, run-time verification and white box test generation are already commercially successful. For example, the Ballistic Missile Defense Project is using our tools instead of their initial plans to use IBM/Rational Rose Real-time. Time Rover's tools are the only formal specification, run-time verification, and white box test generation tools that have been successful on a commercial basis.
We believe that support for system-level and environment modeling languages and tools, as specified in this proposal will appeal to many system level developers concerned with safety critical applications.

NASA's technology taxonomy has been developed by the SBIR-STTR program to disseminate awareness of proposed and awarded R/R&D in the agency. It is a listing of over 100 technologies, sorted into broad categories, of interest to NASA.

TECHNOLOGY TAXONOMY MAPPING
Operations Concepts and Requirements
Simulation Modeling Environment
Testing Facilities
Testing Requirements and Architectures


Form Printed on 09-19-05 13:12