Skip to Main content Skip to Navigation

Probabilistic Contracts for Component-based Design

Gregor Gössler 1 Dana Xu 2 Alain Girault 1
1 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG [2007-2015] - Laboratoire d'Informatique de Grenoble [2007-2015]
Abstract : We define a probabilistic contract framework for describing and analysing component-based embedded systems, based on the theory of Interactive Markov Chains (IMC). A contract specifies the assumptions a component makes on its context and the guarantees it provides. Probabilistic transitions allow for uncertainty in the component behavior, e.g., to model observed black-box behavior (internal choice) or reliability. An interaction model specifies how components interact. We provide the ingredients for a component-based design flow, including (1) contract satisfaction and refinement, (2) parallel composition of contracts over disjoint, interacting components, and (3) conjunction of contracts describing different requirements over the same component. Compositional design is enabled by congruence of refinement.
Complete list of metadatas
Contributor : Gregor Gössler <>
Submitted on : Tuesday, October 1, 2013 - 8:56:13 AM
Last modification on : Friday, July 17, 2020 - 11:10:25 AM
Long-term archiving on: : Wednesday, October 10, 2012 - 2:25:50 AM


Files produced by the author(s)


  • HAL Id : inria-00507785, version 2



Gregor Gössler, Dana Xu, Alain Girault. Probabilistic Contracts for Component-based Design. [Research Report] RR-7328, INRIA. 2012. ⟨inria-00507785v2⟩



Record views


Files downloads