Sagar Chaki

Sagar Chaki, James Edmondson, Proceedings of the ACM/IEEE 17th International Conference on Model Driven Engineering Languages and Systems (MODELS), Sep 28-Oct 3, 2014, Valencia, Spain.

Software: Tools and benchmarks for experiments reported in the paper are here. Read LICENSE.txt for the license, and README.txt for usage.

Abstract: We present an approach, based on model-driven verifying compilation, to construct distributed applications that satisfy user-specified safety specifications, assuming a "synchronous network" model of computation. Given a distributed application P_s and a safety specification Spec in a domain specific language DASL (that we have developed), we first use a combination of sequentialization and software model checking to verify that P_d satisfies Spec. If verification succeeds, we generate a C++ implementation of P_d that targets the MADARA middleware. The generated code uses a novel barrier-based synchronizer protocol (that we have also developed) to implement the synchronous network semantics over a physical network, which is ultimately asynchronous. We formally present the syntax and semantics of DASL. We also present, and prove correctness of, two flavors of sequentialization and the synchronizer protocol. Finally, we evaluate the two sequentializations empirically on a collection of distributed applications with safety-critical requirements.