Bounded Synthesis of Synchronized Distributed Models from Lightweight Specifications
Pablo F. Castro, Luciano Putruele, Renzo Degiovanni, Nazareno Aguirre
TL;DR
The paper tackles the problem of automatically synthesizing synchronized distributed models from lightweight local specifications, under a global LTL constraint $\phi$. It combines bounded model finding with a guarded-command synthesis pipeline: Alloy enumerates component implementations up to a bound $k$, which are then composed asynchronously and checked against $\phi$ (via a model checker like NuSMV). To mitigate exponential search, it introduces a counterexample-guided, batch-based refinement: batches of counterexamples prune infeasible local implementations, and refinements are propagated through refined specifications $\text{Ref}(\text{PS},T)$. The approach is sound within the chosen bound and demonstrates practical effectiveness on standard distributed algorithms, with a prototype tool comparing favorably to related methods in several benchmarks, especially when the number of shared variables is modest.
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.