Skip to Main content Skip to Navigation

Compositional Reasoning on (Probabilistic) Contracts

Benoît Delahaye 1 Benoit Caillaud 1 Axel Legay 1 
1 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : In this paper, we focus on Assume/Guarantee contracts consisting in (i) a non deterministic model of components behaviour, and (ii) a stochastic and non deterministic model of systems faults. Two types of contracts capable of capturing reliability and availability properties are considered. We show that Satisfaction and Refinement can be checked by effective methods thanks to a reduction to classical verification problems on Markov Decision Processes and transition systems. Theorems supporting compositional reasoning and enabling the scalable analysis of complex systems are also detailed in the paper.
Document type :
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Benoît Delahaye Connect in order to contact the contributor
Submitted on : Thursday, June 25, 2009 - 3:02:09 PM
Last modification on : Friday, February 4, 2022 - 3:25:01 AM
Long-term archiving on: : Tuesday, June 15, 2010 - 6:49:05 PM


Files produced by the author(s)


  • HAL Id : inria-00398985, version 1


Benoît Delahaye, Benoit Caillaud, Axel Legay. Compositional Reasoning on (Probabilistic) Contracts. [Research Report] RR-6970, INRIA. 2009. ⟨inria-00398985⟩



Record views


Files downloads