Compositional Contract Abstraction for System Design

Albert Benveniste 1 Dejan Nickovic 2 Thomas Henzinger 3
1 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 AIT
AIT - Austrian Institute of Technology [Vienna]
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
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-00938854
Contributor : Albert Benveniste <>
Submitted on : Wednesday, January 29, 2014 - 4:30:53 PM
Last modification on : Thursday, February 7, 2019 - 5:54:09 PM
Long-term archiving on : Wednesday, April 30, 2014 - 7:55:11 AM

File

RR-8460.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00938854, version 1

Citation

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

Share

Metrics

Record views

1408

Files downloads

333