Skip to Main content Skip to Navigation
Journal articles

Probabilistic contracts for component-based design

Gregor Goessler 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 - Laboratoire d'Informatique de Grenoble [2007-2015]
Abstract : We define a framework of probabilistic contracts for constructing component-based embedded systems, based on the formalism of discrete-time Interactive Markov Chains. A contract specifies the assumptions a component makes on its context and the guarantees it provides. Probabilistic transitions represent allowed uncertainty in the component behavior, for instance, to model internal choice or reliability. Action transitions are used to model non-deterministic behavior and communication between components. An interaction model specifies how components interact with each other. 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.
Document type :
Journal articles
Complete list of metadatas
Contributor : Gregor Gössler <>
Submitted on : Wednesday, October 31, 2012 - 5:05:37 PM
Last modification on : Thursday, July 9, 2020 - 9:44:35 AM

Links full text





Gregor Goessler, Dana Xu, Alain Girault. Probabilistic contracts for component-based design. Formal Methods in System Design, Springer Verlag, 2012, 41 (2), pp.211-231. ⟨10.1007/s10703-012-0162-4⟩. ⟨hal-00747620⟩



Record views