Probabilistic Contracts for Component-Based Design

10 years 2 months ago
Probabilistic Contracts for Component-Based Design
Abstract. We define a probabilistic contract framework for the construction of component-based embedded systems, based on the theory of Interactive Markov Chains. 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.
Dana N. Xu, Gregor Gößler, Alain Giraul
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where ATVA
Authors Dana N. Xu, Gregor Gößler, Alain Girault
Comments (0)