PROPOSAL NUMBER: | 05-II X5.01-9960 |
PHASE-I CONTRACT NUMBER: | NNA06AA17C |
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, Inc.
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) 507-2684
TECHNICAL ABSTRACT (Limit 2000 characters, approximately 200 words)
This proposal is for the creation of a system-level software specification and verification tool. This proposal suggests a major leap-forward in usability of modeling, code generation, Runtime Verification (RV), and Automatic Test Generation (ATG) from the component-level to the system-level.
1. We will create a specification and run-time verification environment for system-level specifications using J-MSC assertions and distributed assertions. J-MSC assertions are a UML-based system-level formal specification language. In phase-I we demonstrated J-MSC assertion and distributed assertion specification and monitoring. In phase-II we will construct an editor, code-generator, and run-time monitor for J-MSC assertions and for distributed assertions.
2. We will create system-level verification environment, compliant with the de-facto JUnit testing framework, including:
? RV of J-MSC assertions for system verification combined with statechart-assertions for the component level.
? RV of distributed assertions.
? System-level white-box ATG of UML controller models and assertions: white-box ATG for a plurality controller modules and for a plurality of controller instances.
? Combined black-box/Matlab and white-box ATG, with support for both open-loop and closed loop techniques.
? White-box ATG based on real-time contracts of system components.
POTENTIAL NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 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 are primarily component-level. In fact, the prevailing NASA organizational approach separates Matlab modeling from embedded-software development and verification, with separate teams working on those respective issues. Robust system-level verification that is also combined with Matlab environment data will provide significant improvement to the level of NASA's system and software safety in two respects: (i) raising the level of specification and verification from the component-level to the verification-level, and (ii) real-life Matlab environment models created by the Matlab modeling team will be usable in conjunction with robust formal methods for the verification of embedded software.
POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
Time Rover's component-level, UML-based, modeling, specification, RV, and WBATG, are already commercially successful. For example, the Ballistic Missile Defense (BMD) project is using our tools instead of their initial plans to use IBM/Rational Rose Real-time. Time Rover's tools are the only such tools that have been successful on a commercial basis. The BMD is distributed in nature and therefore deserves system-level specification and verification techniques that rise above the component level, as suggested by this proposal.
In addition, we see an emerging market of V&V of safety critical applications, which include: DoD related projects (automated army and navy safety critical embedded software control), civilian aerospace avionics and air-traffic control, railway control, and power generation and distribution control.
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 Software Tools for Distributed Analysis and Simulation Testing Requirements and Architectures |