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.
Type de document :
[Research Report] RR-6970, INRIA. 2009
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger
Contributeur : Benoît Delahaye <>
Soumis le : jeudi 25 juin 2009 - 15:02:09
Dernière modification le : mercredi 16 mai 2018 - 11:23:05
Document(s) archivé(s) le : mardi 15 juin 2010 - 18:49:05


Fichiers produits par l'(les) auteur(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〉



Consultations de la notice


Téléchargements de fichiers