Emile: The EventML Explorer

Award Information
Agency:
National Aeronautics and Space Administration
Amount:
$699,932.00
Program:
SBIR
Contract:
NNX13CL03C
Solitcitation Year:
2011
Solicitation Number:
N/A
Branch:
N/A
Award Year:
2013
Phase:
Phase II
Agency Tracking Number:
114127
Solicitation Topic Code:
A1.20
Small Business Information
Odyssey Research Assoc Inc
NY, Ithaca, NY, 14850-1279
Hubzone Owned:
N
Woman Owned:
N
Socially and Economically Disadvantaged:
N
Duns:
101321479
Principal Investigator
 David Guaspari
 Principal Investigator
 (607) 257-1975
 davidg@atc-nycorp.com
Business Contact
 Richard Smith
Title: Business Official
Phone: (607) 257-1975
Email: rick@atc-nycorp.com
Research Institution
 Stub
Abstract
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." Properties of EventML protocols can be formally verified by interactive theorem proving in the Nuprl environment. To integrate these conceptual tools with standard processes of system development, and to make the labor intensive task of verifying protocol properties more efficient, ATC-NY is developing Emile. Emile is a software tool that provides: a semantic interface to EventML that translates assertions about properties of EventML programs into logical forms to which powerful fully automated analysis tools can be applied, along with a "logical manager" that can direct analyses involving the interaction of these tools. We will demonstrate Emile by using it to verify the key properties of EventML source code for standard consensus algorithms, such as Paxos.

* information listed above is at the time of submission.

Agency Micro-sites

US Flag An Official Website of the United States Government