DS2 Arch DS2 stands for Distributed Systems Domain Specific Language. The advent of distributed systems in all scales, from clouds to IoT, lead for it to become mainstream. The lack of formal methods support added to both untrained mainstream developers and extreme difficulty of correctly designed distributed systems lead to the need for principled approaches to address the issue. DS2 tries to first address the correctness, testing and exploration aspects of distributed systems by providing practitioners with verification infrastructure and tools aiding them build systems faster and with more correctness guarantees. In addition, the ultimate goal is to lift most, if not all, of the hurdles of distributed systems development from programmers shoulders and provide them with a full stack of domain specific language with all facilities they need to explore their systems and reason about them.


  • Currently code can't be released till further notice. If you are looking for benchmarks we developed, please look at the projects and reports section.


ACM DL Author-ize serviceToward rigorous design of domain-specific distributed systems
Mohammed Al-Mahfoudh, Ganesh Gopalakrishnan, Ryan Stutsman
FormaliSE '16 Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering, 2016.[bib]
Toward Bringing Distributed Systems Design upon Rigorous Footing, Mohammed S. Al-Mahfoudh , Ganesh Gopalakrishnan, Ryan Stutsman [bib]

Operational Semantics for the Rigorous Analysis of Distributed Systems, Mohammed S. Al-Mahfoudh , Ganesh Gopalakrishnan, Ryan Stutsman [bib]

Projects and Reports


  • Distributed Systems Abstract Model: "DS2 Operational Semantics TR" is a technical report detailing the operational semantics of our generic distributed systems model based on Akka Actors. NOTE: this document is under constant development and updates keep being added as code is modified accordingly.
  • Operational Semantics for Distributed Systems Full Runtime Snapshot and Resume (COMING SOON): A technical report detailing the operational semantics used to snapshot the complete runtime state of a distributed system and its scheduler using a two phase two split copy-link operation and restoring to that state.


Related Work

The Parachute Project