Compositional Contract Abstraction for System Design

Albert Benveniste 1 Dejan Nickovic 2 Thomas Henzinger 3
1 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 AIT
AIT - Austrian Institute of Technology [Vienna]
Résumé : La conception par contrats a été proposée récemment comme une approche formelle pour la conception de systèmes permettant le développement parallèle de sysèmes dans un contexte de chaine complexe de sous-traitants. Les théories d'interfaces, les interfaces modales et les contrats hypothèse/garantie, sont autant de formalismes en ce sens. L'article collectif [Benveniste et al. 2012] a proposé une "méta-théorie" des contrats, unifiant les formalismes précédents. Le présent rapport développe, pour cette méta-théorie des contrats, une technique systématique d'abstraction. Les propriétés fondamentales des contrats (relation d'implémentation, d'environnement, de raffinement) peuvent être prouvées sur les abstractions. L'abstraction proposée offre de bonnes propriétés de compositionnalité, même si toutes les propriétés souhaitables ne sont pas valides. Cette technique d'abstraction complète celle des observateurs, qui permettent d'invalider des propriétés de contrats par une approche de type test. Mots-clés : conception des systèmes, composant, contrat, interface, abstraction, interprétation abstraite.
Type de document :
Rapport
[Research Report] RR-8460, INRIA. 2014
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00938854
Contributeur : Albert Benveniste <>
Soumis le : mercredi 29 janvier 2014 - 16:30:53
Dernière modification le : mardi 16 janvier 2018 - 15:54:23
Document(s) archivé(s) le : mercredi 30 avril 2014 - 07:55:11

Fichier

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

Identifiants

  • HAL Id : hal-00938854, version 1

Citation

Albert Benveniste, Dejan Nickovic, Thomas Henzinger. Compositional Contract Abstraction for System Design. [Research Report] RR-8460, INRIA. 2014. 〈hal-00938854〉

Partager

Métriques

Consultations de la notice

958

Téléchargements de fichiers

260