Compositional Reasoning on (Probabilistic) Contracts
Benoît Delahaye, Benoı̂t Caillaud, Axel Legay · 2009
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 Refine-ment 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 de-tailed in the paper. 1.