Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/inria-00554307
Contributor : Benoît Caillaud <>
Submitted on : Monday, January 10, 2011 - 3:50:01 PM
Last modification on : Tuesday, June 15, 2021 - 4:27:42 PM

Links full text

Identifiers

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⟩

Share

Metrics

Record views

698