Refinement-based Synthesis of Correct Contract Model Decompositions

In distributed development of modern systems, contracts play a vital role in ensuring interoperability of components and adherence to specifications. It is therefore often desirable to verify the satisfaction of an overall property represented as a contract, given the satisfaction of smaller properties also represented as contracts. When the verification result is negative, designers must face the issue of refining the sub-properties and components. This is an instance of the classical synthesis problems: 'can we construct a model that satisfies some given specification?'. In this work, we propose a strategy enabling designers to synthesize or refine a set of contracts so that their composition satisfies a given contract. We develop a generic algebraic method, and show how it can be applied in different contract models to support top-down component-based development of distributed systems.