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

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.

Domaines: Autre [cs.OH]

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, 2011, 38 (1), pp.1-32. ⟨10.1007/s10703-010-0107-8⟩. ⟨inria-00554307⟩