PRL Seminars 2002-2003

Abstract

We will talk about work in progress that provides a method for extracting correct-by-construction distributed algorithms from constructive proofs of specifications about events in space and time. We propose logical rules about events that are justified by an operational semantics for IO automata which become the realizers of logical statements.

This approach leads to relatively succinct specifications of well-known distributed algorithms. The event model incorporates basic assumptions about the nature of time and causality in distributed systems. The logic provides natural declarative ways to combine specifications, and the extraction rules convert these into composition of automata.

The logic supports top down proof and a corresponding top down development of protocols and systems which satisfy the specifications. We have used this method to derive by hand simple algorithms, such as leader election, in ways that are beyond the capability of the formal methods for verifying properties of IO automata that we have been using until now.