Model-Driven Verifying Compilation of Synchronous Distributed Applications.

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 Pd and a safety specification. 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 phi. If verification succeeds, we generate an implementation of P-d that uses a novel barrier- based synchronizer protocol (that we have also developed) to implement the synchronous network semantics. We present the syntax and semantics of dasl. We also present, and prove correctness of, two sequentialization algorithms, and the synchronizer protocol. Finally, we evaluate the two sequentializations on a collection of distributed applications with safety- critical requirements.