Distributed Systems and Event Logic

In collaboration with Cornell University Computer Science we have defined a logic of events for the formal specification and analysis of distributed protocols [Bic05b]. Event logic allows the derivation of correct-by-construction distributed algorithms.

High-level specifications in event logic are purely declarative—describing what behavior is desired but not how that is achieved. Declarative specifications are often easier to understand than lower level specifications that are algorithmic or operational. To implement a specification we use the NuPrl logical programming environment to prove that it is derivable from basic rules and lemmas in our library (logically speaking, we prove that there exists some system that meets the specification)—and from the proof we automatically extract the code for system. We currently extract Java code, but other target languages can also be supported.

Related work, [Liu01, Bic01], analyzes a generic protocol switching algorithm in order to formally characterize the properties that are preserved while switching from one protocol to another. That allows us to build adaptive protocols that change switch between protocol implementations while preserving key consistency properties.

References

[Bic05b] M. Bickford and R.L. Constable. A Causal Logic of Events in Formalized Computational Type Theory. Cornell University Technical Report, 2005. http://www.nuprl.org/documents/Bickford/TechReportCLEinCTT.html

[Liu01] X. Liu, R. van Renesse, M. Bickford, C. Kreitz, R.L. Constable. Protocol Switching: Exploiting Meta-Properties. ICDS Workshops, 2001, pp. 37-42. http://www.nuprl.org/documents/Liu/01wargc-switching.html

[Bic01] M. Bickford, C. Kreitz, R. van Renesse, and X. Liu. Proving Hybrid Protocols Correct. TPHOLS 2001, pp. 105-120. http://www.nuprl.org/documents/Bickford/01tphols-hybridcorrect.html