Probabilistic Contracts for Component-based Design

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.
Type de document :
Rapport
[Research Report] RR-7328, INRIA. 2012
Liste complète des métadonnées

https://hal.inria.fr/inria-00507785
Contributeur : Gregor Gössler <>
Soumis le : mardi 1 octobre 2013 - 08:56:13
Dernière modification le : samedi 17 septembre 2016 - 01:39:26
Document(s) archivé(s) le : mercredi 10 octobre 2012 - 02:25:50

Fichier

RR-7328.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00507785, version 2

Collections

Citation

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

Partager

Métriques

Consultations de
la notice

327

Téléchargements du document

124