Compositional Reasoning on (Probabilistic) Contracts

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