Compositional Contract Abstraction for System Design

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 in [Benveniste et al. 2012], 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 [6]. The latter allow disproving properties, whereas abstraction allows proving them. Key-words: system design, component based design, contract, interface, abstraction, abstract interpretation.La conception par contrats a été proposée récemment comme une approche formelle pour la conception de systèmes permettant le développement parallèle de sysèmes dans un contexte de chaine complexe de sous-traitants. Les théories d'interfaces, les interfaces modales et les contrats hypothèse/garantie, sont autant de formalismes en ce sens. L'article collectif [Benveniste et al. 2012] a proposé une "méta-théorie" des contrats, unifiant les formalismes précédents. Le présent rapport développe, pour cette méta-théorie des contrats, une technique systématique d'abstraction. Les propriétés fondamentales des contrats (relation d'implémentation, d'environnement, de raffinement) peuvent être prouvées sur les abstractions. L'abstraction proposée offre de bonnes propriétés de compositionnalité, même si toutes les propriétés souhaitables ne sont pas valides. Cette technique d'abstraction complète celle des observateurs, qui permettent d'invalider des propriétés de contrats par une approche de type test. Mots-clés : conception des systèmes, composant, contrat, interface, abstraction, interprétation abstraite