Bounded Synthesis of Synchronized Distributed Models from Lightweight Specifications

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.