Bounded Synthesis of Synchronized Distributed Models from Lightweight Specifications

TL;DR

This paper introduces a bounded synthesis method for automatically generating synchronized distributed models from lightweight specifications, combining Alloy encoding, model checking, and counterexample-guided pruning to efficiently produce correct models.

Contribution

It presents a novel bounded synthesis algorithm that uses counterexamples to prune the search space, improving the efficiency of generating synchronized distributed models from lightweight specifications.

Findings

The approach is sound within the chosen bounds.

Counterexample batching effectively reduces search space.

Prototype implementation demonstrates practical viability.

Abstract

We present an approach to automatically synthesize synchronized models from lightweight formal specifications. Our approach takes as input a specification of a distributed system along with a global linear time constraint, which must be fulfilled by the interaction of the system's components. It produces executable models for the component specifications (in the style of Promela language) whose concurrent execution satisfies the global constraint. The component specifications consist of a collection of actions described by means of pre and post conditions together with first-order relational formulas prescribing their behavior. We use the Alloy Analyzer to encode the component specifications and enumerate their potential implementations up to some bound, whose concurrent composition is model checked against the global property. Even though this approach is sound and complete up to the selected bound, it is impractical as the number of candidate implementations grows exponentially. To address this, we propose an algorithm that uses batches of counterexamples to prune the solution space, it has two main phases: exploration, the algorithm collects a batch of counterexamples, and exploitation, where this knowledge is used to speed up the search. The approach is sound, while its completeness depends on the batches used. We present a prototype tool, describe some experiments, and compare it with related approaches.