28623 articles – 22140 references  [version française]

hal-00715750, version 1

Probabilistic Contracts for Component-based Design

Gregor Gössler () a1, Dana N. Xu () a2, Alain Girault () a1

N° RR-7328 (2012)

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.

  • a –  INRIA
  • 1:  POP ART (INRIA Grenoble Rhône-Alpes / LIG Laboratoire d'Informatique de Grenoble)
  • INRIA – Institut polytechnique de Grenoble (Grenoble INP) – Université Joseph Fourier - Grenoble I – Université Pierre-Mendès-France - Grenoble II – CNRS : UMR5217
  • 2:  GALLIUM (INRIA Rocquencourt)
  • INRIA
  • Domain : Computer Science/Formal Languages and Automata Theory
    Computer Science/Embedded Systems
  • Internal note : RR-7328
 
  • hal-00715750, version 1
  • oai:hal.inria.fr:hal-00715750
  • From: 
  • Submitted on: Monday, 9 July 2012 11:14:21
  • Updated on: Monday, 9 July 2012 16:17:40