Cornell University, USA
4pm Tuesday, 27th October, 2009
Room 4.31/33, Informatics Forum
Experience shows that it is intellectually difficult to specify, design, implement, and safely modify small distributed protocols, even harder than the same tasks for many larger sequential programs. The attempt in the 1990's to build a state-of-the art air traffic control system in the US failed in part because of the difficulty of the these tasks even in the hands of some of the best software companies. Today, efforts to build secure Internet services and distributed data centers for cloud computing depend critically on performing exactly such tasks.
At Cornell we have demonstrated that it is possible to design, implement, and modify distributed protocols that are formally known to perform as required by deriving them automatically from proofs of their properties in a natural very high level Logic of Events. This work is evidence that the Logic of Events captures many fundamental concepts in networked computing.
The lecture will illustrate the correct-by-construction development of a consensus protocol, specifically Paxos. The work is part of our ten year collaboration with the systems group at Cornell. The Logic of Events arose by formalizing the concepts and methods used by system designers, and capturing them in a constructive formal logic that can treat proofs as processes. This event logic has many other applications as well because it can naturally express concepts from the physical and life sciences.