A boolean algebra of contracts for 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 : Contract-based design is an expressive paradigm for a modular and compositional speci cation of programs. It is in turn 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: rst, the assumption or guarantee of a component is de ned as a lter and, second, lters enjoy the structure of a Boolean algebra. This yields a structure of contracts that is a Heyting algebra.
Type de document :
Communication dans un congrès
FACS 2009 : 6th International Workshop on Formal Aspects of Component Software, Nov 2009, Eindhoven, Netherlands. 2009
Liste complète des métadonnées

https://hal.inria.fr/hal-00788413
Contributeur : Ist Rennes <>
Soumis le : jeudi 14 février 2013 - 14:00:33
Dernière modification le : jeudi 11 janvier 2018 - 06:20:09

Identifiants

  • HAL Id : hal-00788413, version 1

Collections

Citation

Yann Glouche, Paul Le Guernic, Jean-Pierre Talpin, Thierry Gautier. A boolean algebra of contracts for assume-guarantee reasoning. FACS 2009 : 6th International Workshop on Formal Aspects of Component Software, Nov 2009, Eindhoven, Netherlands. 2009. 〈hal-00788413〉

Partager

Métriques

Consultations de la notice

107