A Programming Logic for Distributed Systems
Abstract
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 verifiably 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 30, 2005
- Accession Number
- ADA435291
Entities
People
- David Guaspari
- Mark Bickford