Probabilistic Contracts for Component-Based Design

Dana N. Xu 1, * Gregor Goessler 2, * Alain Girault 2
* Auteur correspondant
2 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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.
Type de document :
Communication dans un congrès
the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA), Sep 2010, Singapore, Singapore. Springer, pp.325-340, 2010, 〈10.1007/978-3-642-15643-4_24〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00527169
Contributeur : Na Xu <>
Soumis le : lundi 18 octobre 2010 - 14:33:08
Dernière modification le : vendredi 25 mai 2018 - 12:02:07

Lien texte intégral

Identifiants

Collections

Citation

Dana N. Xu, Gregor Goessler, Alain Girault. Probabilistic Contracts for Component-Based Design. the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA), Sep 2010, Singapore, Singapore. Springer, pp.325-340, 2010, 〈10.1007/978-3-642-15643-4_24〉. 〈inria-00527169〉

Partager

Métriques

Consultations de la notice

269