Probabilistic Contracts : A Compositional Reasoning Methodology for the Design of Systems with Stochastic and/or non-Deterministic Aspects

Benoît Delahaye 1 Benoît 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 : A contract allows to distinguish hypotheses made on a system (the guarantees) from those made on its environment (the assumptions). In this paper, we focus on models of Assume/Guarantee contracts for (stochastic) systems. We consider contracts capable of capturing reliability and availability properties of such systems. We also show that classi- cal notions of Satisfaction and Refinement can be checked by effective methods thanks to a reduction to classical verification problems. Finally, theorems supporting compositional reasoning and enabling the scalable analysis of complex systems are also studied.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2011, 38 (1), pp.1-32. 〈10.1007/s10703-010-0107-8〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00554307
Contributeur : Benoît Caillaud <>
Soumis le : lundi 10 janvier 2011 - 15:50:01
Dernière modification le : mercredi 16 mai 2018 - 11:23:04

Lien texte intégral

istex

Identifiants

Collections

INRIA | IRISA | IRISA-D4 | UR1-UFR-ISTIC | UNIV-RENNES

Citation

Benoît Delahaye, Benoît Caillaud, Axel Legay. Probabilistic Contracts : A Compositional Reasoning Methodology for the Design of Systems with Stochastic and/or non-Deterministic Aspects. Formal Methods in System Design, Springer Verlag, 2011, 38 (1), pp.1-32. 〈10.1007/s10703-010-0107-8〉. 〈inria-00554307〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

463

Contact


archive-ouverte@inria.fr