A Programming Logic for Distributed Systems



by Mark Bickford and David Guaspari

ATC-NY, Technical Report 2005

Abstract

ATC-NY and Cornell University are developing SCorES, a mathe-
matically based tool to support the development of demonstrably cor-
rect distributed systems. SCorES extends to distributed and hybrid
systems a paradigm for program development that has been success-
ful in the world of sequential programming|employing methods that
are declarative (rather than operational) and constructive. Declar-
ative methods permit systems to be speci¯ed, analyzed, developed,
and veri¯ed at a conceptual level congenial to human designers. Con-
structive methods permit automatic code synthesis. Incorporating
these methods within the NuPrl environment provides powerful auto-
mated support for specifying, developing, verifying, and synthesizing
real-time distributed systems at a high level of abstraction.
This report describes two things: a prototype that supports au-
tomatic code generation from proofs in a domain-speci¯c logic of dis-
tributed systems (one that does not model real-time); an extension of
that logic to the domain of hybrid systems, which may contain vari-
ables that vary continuously in real time. We demonstrate the code
generator by deriving a veri¯ably correct leader election protocol; and
we demonstrate the logic of hybrid systems by applying it to a mutual
exclusion algorithm that generalizes Fischer's protocol to distributed
systems.