NASA SBIR 2011 Solicitation
FORM B - PROPOSAL SUMMARY
||Verification and Validation of Flight-Critical Systems
||Emile: The EventML Explorer
SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
Odyssey Research Assoc Inc DBA ATC-NY
33 Thornwood Drive Suite 500
Ithaca, NY 14850 - 1279
PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
David A Guaspari
33 Thornwood Drive, Suite 500
Ithaca, NY 14850 - 1279
Estimated Technology Readiness Level (TRL) at beginning and end of contract:
TECHNICAL ABSTRACT (Limit 2000 characters, approximately 200 words)
The protocols needed to coordinate the activities of distributed components, such as consensus algorithms, are notoriously difficult to design, implement, and verify. Abstraction is the only way to gain intellectual control over this complex problem; so ATC-NY and Cornell University have developed Event Logic, a high-level model for describing and reasoning about distributed systems, and EventML, a high-level functional language for implementing distributed protocols by ?programming with events.? To integrate these conceptual tools with standard processes of system development ATC-NY will develop ?mile, a software tool providing: a semantic interface to EventML that translates assertions about properties of EventML programs into logical forms to which powerful existing analysis tools can be applied, along with a ?logical manager? that can direct analyses involving the interaction of these tools. We will demonstrate ?mile by using it to verify the key properties of EventML source code for standard consensus algorithms, such as Paxos.
POTENTIAL NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
?mile supports the development of critical protocols that underlie highly reliable distributed systems (whether systems are ?naturally? distributed, or replicated for fault tolerance)?for example, air traffic control.
POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
?mile supports the development of critical protocols that underlie highly reliable distributed systems (whether systems are ?naturally? distributed, or replicated for fault tolerance)?for example, the New York Stock Exchange, the AEGIS combat system, Google?s Chubby service (on which Google File System and Google Analytics rely).
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.)
Form Generated on 11-22-11 13:43