A Boolean algebra of contracts for logical assume-guarantee reasoning

Yann Glouche 1 Paul Le Guernic 1 Jean-Pierre Talpin 1 Thierry Gautier 1
1 ESPRESSO - Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Assume-guarantee reasoning is a popular and expressive paradigm for a modular and compositional specification of programs. It is in turn of becoming a fundamental concept in mainstream industrial computer-aided design tools for embedded system design. In this paper, we elaborate new foundations for contract-based embedded system design by proposing a general-purpose algebra of assume/guarantee contracts based on two simple concepts: first, the assumption or guarantee of a component is defined as a filter and, second, filters enjoy the structure of a Boolean algebra. This yields an algebraically rich structure which allows us to reason on contracts.
Type de document :
Rapport
[Research Report] RR-6570, INRIA. 2008, pp.41
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00292870
Contributeur : Yann Glouche <>
Soumis le : mardi 13 janvier 2009 - 15:48:07
Dernière modification le : jeudi 11 janvier 2018 - 06:20:09
Document(s) archivé(s) le : vendredi 24 septembre 2010 - 14:36:20

Fichiers

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

Identifiants

  • HAL Id : inria-00292870, version 7

Citation

Yann Glouche, Paul Le Guernic, Jean-Pierre Talpin, Thierry Gautier. A Boolean algebra of contracts for logical assume-guarantee reasoning. [Research Report] RR-6570, INRIA. 2008, pp.41. 〈inria-00292870v7〉

Partager

Métriques

Consultations de la notice

381

Téléchargements de fichiers

102