NASA SBIR 2010 Solicitation

FORM B - PROPOSAL SUMMARY


PROPOSAL NUMBER: 10-1 X6.01-9065
SUBTOPIC TITLE: Automation for Vehicle and Crew Operations
PROPOSAL TITLE: Formal Verification of Programming by Demonstration Systems

SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
Galois, Inc.
421 SW Sixth Avenue, Suite 300
Portland, OR 97204 - 1622
(503) 626-6616

PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
E. Rogan Creswick
creswick@galois.com
421 SW Sixth Avenue, Suite 300
Portland, OR 97204 - 1622
(503) 808-7195

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

TECHNICAL ABSTRACT (Limit 2000 characters, approximately 200 words)
Automated tools are quickly making inroads into casual computing environments, solving progressively more complex tasks. However, these advancements still require trading reliability for convenience. Frequent minor failures are acceptable in casual environments, but critical systems cannot make the same exchange. The software systems that NASA develops could greatly benefit from machine learning technologies that have been applied to casual computing, if the software developed by learning algorithms could be verified.

We propose to apply formal methods to machine learning, and specifically Programming by Demonstration (PBD). The existing technology readiness level is very low: no known verifiable PBD systems have been deployed and the existing research in the area is limited. The Phase I effort will result in publications and a prototype implementation of a verifiable PBD system using SMT solvers. Phase II will build on Phase I publications and prototypes to demonstrate increased verification capabilities through the application of more complex formal methods, such as model checking. Verifiable machine learning would allow for trainable systems that meet critical properties, but are still adaptable to specific use cases. Such tools could be re-purposed for multiple applications without incurring the development costs associated with manual automation techniques today.

POTENTIAL NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
Crew-facing tools, remote control systems, and stored procedure authoring could all benefit from the capabilities offered by programming by demonstration and machine learning. Enabling these technologies to be applied safely will open up many opportunities at NASA for application re-use and productivity improvements through customization and fast, robust, macro/procedure creation. Improving automation in these areas will allow for more complex stored procedures to be used on un-manned craft and manned craft can take advantage of greater robustness through increasingly complex automatic navigation. Customization benefits will enable astronauts and remote operators to train general purpose tools (such as robotic arms) to perform complex repetitive operations at the press of a button simply by demonstrating the task a few times. These technologies have the potential to greatly increase the speed and reliability of NASA mission control, sample collection, and repair work.

POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
Machine learning and automation tools extend into all industries, bringing about improved human-computer interactions through per-user and per-task customization. While many tools have already been applied to casual computer use, there are myriad domains that have yet to adopt learning techniques because of the absence of behavioral guarantees. For example, reliable human review to ensure information assurance, remote piloting of UAVs, and even system administration tasks all require high levels of reliability, yet these tasks are also rife with meticulous and error-prone tasks that currently must be performed by trained experts. Formally verified learning tools will be able to address these needs without increasing the risk associated with automation today.

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.)
Analytical Methods
Intelligence
Man-Machine Interaction


Form Generated on 09-03-10 12:12