Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/inria-00398985
Contributor : Benoît Delahaye <>
Submitted on : Thursday, June 25, 2009 - 3:02:09 PM
Last modification on : Tuesday, June 15, 2021 - 4:14:02 PM
Long-term archiving on: : Tuesday, June 15, 2010 - 6:49:05 PM

Files

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

Identifiers

  • HAL Id : inria-00398985, version 1

Citation

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

Share

Metrics

Record views

507

Files downloads

260