Toward Rigorous Design of Domain-Specific Distributed Systems

The advent of data center, cloud computing and IoT has thrust distributed systems building into the programming mainstream. Building correct distributed systems is notoriously hard, yet today's developers have little training and few tools to aid them in reasoning about these complex systems. To that end, we present DS2 - a domain-specific language and integrated framework for specifying, synthesizing, and reasoning. The DS2 language is parsimonious, and comes with an operational semantics that lends semantic clarity and enables formal analysis. A variety of techniques for model exploration, active testing, and synthesis of detailed implementations from higher level specifications are being developed. This paper details these aspects of DS2 and provides a roadmap of its evolution.