Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Compositional Contract Abstraction for System Design

Abstract : 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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Albert Benveniste Connect in order to contact the contributor
Submitted on : Wednesday, January 29, 2014 - 4:30:53 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:23 AM
Long-term archiving on: : Wednesday, April 30, 2014 - 7:55:11 AM


Files produced by the author(s)


  • HAL Id : hal-00938854, version 1


Albert Benveniste, Dejan Nickovic, Thomas Henzinger. Compositional Contract Abstraction for System Design. [Research Report] RR-8460, INRIA. 2014. ⟨hal-00938854⟩



Record views


Files downloads