NASA SBIR 2012 Solicitation

FORM B - PROPOSAL SUMMARY


PROPOSAL NUMBER: 12-1 A1.06-8686
SUBTOPIC TITLE: Assurance of Flight-Critical Systems
PROPOSAL TITLE: Scalable Parallel Algorithms for Formal Verification of Software

SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
Aries Design Automation, LLC
2705 W Byron Street
Chicago, IL 60618 - 3745
(773) 856-6633

PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
Miroslav N. Velev
miroslav.velev@aries-da.com
2705 W Byron Street
Chicago, IL 60618 - 3745
(773) 856-6633

CORPORATE/BUSINESS OFFICIAL (Name, E-mail, Mail Address, City/State/Zip, Phone)
Miroslav N. Velev
miroslav.velev@aries-da.com
2705 W Byron Street
Chicago, IL 60618 - 3745
(773) 856-6633

Estimated Technology Readiness Level (TRL) at beginning and end of contract:
Begin: 3
End: 4

Technology Available (TAV) Subtopics
Assurance of Flight-Critical Systems is a Technology Available (TAV) subtopic that includes NASA Intellectual Property (IP). Do you plan to use the NASA IP under the award?
No

TECHNICAL ABSTRACT (Limit 2000 characters, approximately 200 words)
We will develop an efficient Graphics Processing Unit (GPU) based parallel Binary Decision Diagram (BDD) software package, and will also combine it with our GPU-based parallel SAT solver that we are currently developing in a NASA SBIR Phase II project in order to solve much larger and more complex Boolean formulas from formal verification than possible with either method alone. BDDs are a data structure that satisfies some simple restrictions, resulting in a unique representation of a Boolean function regardless of its actual implementation. This property of BDDs allows the efficient solution of many problems. The proposed tool will exploit multi-core CPUs and the thousands of stream cores in the latest GPUs, which were made accessible to programmers through specialized software development kits. These large numbers of stream cores in GPUs, and the possibility to execute non-graphics computations on them, open unprecedented levels of parallelism at a very low cost. In the last 8 years, GPUs had an increasing performance advantage of an order of magnitude relative to x86 CPUs. Furthermore, this performance advantage will continue to increase in the next 20 years because of the scalability of the chip manufacturing processes. The technical objectives will be to efficiently exploit the GPU parallelism in order to accelerate the execution of our prototype GPU-based parallel BDD package, and to implement hybrid approaches combining it with our GPU-based parallel SAT solver. BDDs and SAT solvers are orthogonal methods with different advantages, and a hybrid of the two will significantly increase both the speed and capacity when formally verifying complex software for space missions. We achieved at least 2 orders of magnitude speedup with our prototype GPU-based parallel BDD package in a previous Phase I, and expect to achieve at least 4 orders of magnitude speedup with our hybrid BDD-SAT tool by the end of Phase II, compared to the current state of the art.

POTENTIAL NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
Efficiently solving of challenging Boolean formulas is critical to NASA, as this will increase both the speed and scalability of the following applications:
1) formal verification and testing methods for complex mission software and hardware, including those of the Multi-Purpose Crew Vehicle (MPCV), the next generations of Mars Rovers, and other spacecraft;
2) formal methods to prove the correctness of radiation-hardening transformations for software and hardware;
3) logic synthesis of circuits;
4) Boolean methods for scheduling, planning, and solving of other Constraint Satisfaction Problems (CSPs);
5) formal methods for network coding that will increase both the bandwidth and reliability of space communications by using the existing communication equipment that is already deployed in space after updating the firmware;
6) reliability analysis of hardware, software, and mechanical systems;
7) power and timing analysis of circuits;
8) design of experiments;
9) design of error-correction codes;
10) technology mapping and routing for FPGAs and other reconfigurable circuits;
11) formal methods for cryptanalysis; and
12) cyber security---detecting security vulnerabilities and malicious intent in software.

POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
The potential non-NASA commercial applications include:
1) Formal verification and testing of software and hardware, where the potential customers will be all major semiconductor and software companies.
2) Scheduling, planning, and solving of Constraint Satisfaction Problems (CSPs), where the potential customers will be all companies that use scheduling and planning tools.
3) Solving of Electronic Design Automation (EDA) problems, such as FPGA technology mapping and routing, power and timing analysis of circuits, and formal methods to check the robustness of radiation-hardened circuits, where the potential customers will be all EDA and semiconductor companies.
4) Formal methods for cryptanalysis, where the potential customers will be the Department of Defense, the NSA, and all companies that use cryptanalysis.
5) Formal methods for cyber security, such as for detection of security vulnerabilities and malicious intent in software, where the potential customers will be all companies that develop robust virus scanners based on formal methods, and companies that develop formal methods for detecting security vulnerabilities in software. Because of the potential for a very wide range of software obfuscations that can be used to hide malicious intent, future virus scanners will have to employ efficient formal methods to detect malware, and thus the importance of speed and scalability that will be possible with an efficient hybrid BDD-SAT tool.

TECHNOLOGY TAXONOMY MAPPING (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.)
Air Transportation & Safety
Algorithms/Control Software & Systems (see also Autonomous Systems)
Analytical Methods
Architecture/Framework/Protocols
Circuits (including ICs; for specific applications, see e.g., Communications, Networking & Signal Transport; Control & Monitoring, Sensors)
Coding & Compression
Command & Control
Computer System Architectures
Data Modeling (see also Testing & Evaluation)
Development Environments
Models & Simulations (see also Testing & Evaluation)
Operating Systems
Programming Languages
Project Management
Prototyping
Simulation & Modeling
Software Tools (Analysis, Design)
Space Transportation & Safety
Spacecraft Design, Construction, Testing, & Performance (see also Engineering; Testing & Evaluation)
Verification/Validation Tools


Form Generated on 03-28-13 15:21