Probabilistic Contracts : A Compositional Reasoning Methodology for the Design of Systems with Stochastic and/or non-Deterministic Aspects

Delahaye, Benoît;Caillaud, Benoît;Legay, Axel
(2011) Formal Methods in System Design : an international journal —

Files

No attached file found for this publication.

Details

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

Citations

  • APA
  • Chicago
  • FWB

Delahaye, B., Caillaud, B., & Legay, A. (2011). Probabilistic Contracts : A Compositional Reasoning Methodology for the Design of Systems with Stochastic and/or non-Deterministic Aspects. Formal Methods in System Design : an international journal. https://doi.org/10.1007/s10703-010-0107-8