Compositional Reasoning on (Probabilistic) Contracts

Delahaye, Benoît;Caillaud, Benoit;Legay, Axel
(2009)

Files

No attached file found for this publication.

Details

Authors
  • Delahaye, Benoît
    Author
  • Caillaud, Benoit
    Author
  • Legay, AxelUCLouvain
    Author
Abstract
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.

Citations

  • APA
  • Chicago
  • FWB

Delahaye, B., Caillaud, B., & Legay, A. (2009). Compositional Reasoning on (Probabilistic) Contracts. https://hdl.handle.net/2078.5/173052