Contract-based design has been recently proposed as a framework for concurrent system design in the context of complex supplier chains, where sub-system design can be sub-contracted to suppliers while guaranteeing correct system integration. A unifying meta-theory of contracts was proposed by a superset of these authors, which subsumes known frameworks such as interface theories, modal interfaces, and Assume/Guarantee contracts. This report proposes, for this meta-theory of contracts, a generic abstraction technique allowing to prove contract properties based on their abstractions. More precisely, we show how to lift abstractions, from components to contracts, in a systematic way. In doing so, fundamental relations such as being a correct implementation or a valid environment, refining, can be checked on abstractions. Our abstraction technique is fully compositional with respect to contract conjunction. Compositionality of abstraction with respect to contract composition is only partially achieved. We believe that the results we obtain are the best achievable ones and we explain the obstructions we see against improving them. Our abstraction technique complements observers, proposed as a testing technique adapted to contracts in the above mentioned reference. The latter allow disproving properties, whereas abstraction allows proving them.

Key-words: system design, component based design, contract, interface, abstraction, abstract interpretation.

Link to HAL repository