Contract-based requirement modularization via synthesis of correct decompositions

n distributed development of modern systems, contracts play a vital role in ensuring interoperability ofcomponents and adherence to specifications. It is therefore often desirable to verify the satisfaction of anoverall property represented as a contract, given the satisfaction of smaller properties also represented ascontracts. When the verification result is negative, designers must face the issue of refining the subpropertiesand components. This is an instance of the classical synthesis problems: “can we construct a model thatsatisfies some given specification?” In this work, we propose two strategies enabling designers to synthesizeor refine a set of contracts so that their composition satisfies a given contract. We develop a generic algebraicmethod and show how it can be applied in different contract models to support top-down component-baseddevelopment of distributed systems.