← Back to NASA Technology Projects
Completed TRL 6 (started at 3, targeting 6)
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.
Emile 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.
Examples of non-NASA Commercial Applications requiring the support Emile provides for highly reliable distributed systems include the New York Stock Exchange, the AEGIS combat system, Google's Chubby service (on which Google File System and Google Analytics rely).
Listed on TechPort itself — the most direct way to ask about this specific project.
This is early/mid-stage (TRL 6) — the most realistic path in is NASA SBIR/STTR, which funds small businesses and research institutions to develop technology aligned with NASA's needs (equity-free, phased funding). Check whether a current SBIR/STTR solicitation topic overlaps with this project's technology area, or contact the project directly (above) to ask.
None of these are guaranteed paths for this specific project — TechPort itself doesn't have an "apply" button. Reaching out to the contact(s) above with a specific question is usually the fastest way to find out what's actually open.