A Programming Logic for Distributed Systems
by Mark Bickford, David Guaspari
ATC-NY Technical Report
ATC-NY and Cornell University are developing SCorES, a mathematically based tool to support the development of demonstrably correct distributed systems. SCorES extends to distributed and hybrid systems a paradigm for program development that has been successful in the world of sequential programming employing methods that are declarative (rather than operational) and constructive. Declarative methods permit systems to be specified, analyzed, developed, and verified at a conceptual level congenial to human designers. Constructive methods permit automatic code synthesis. Incorporating these methods within the NuPrl environment provides powerful automated 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 automatic code generation from proofs in a domain-specific logic of distributed systems (one that does not model real-time); an extension of that logic to the domain of hybrid systems, which may contain variables that vary continuously in real time. We demonstrate the code generator by deriving a verifyably 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.
bibTex ref: BG05