Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download
Contributor : Yann Glouche Connect in order to contact the contributor
Submitted on : Tuesday, January 13, 2009 - 3:48:07 PM
Last modification on : Thursday, October 27, 2022 - 3:45:22 AM
Long-term archiving on: : Friday, September 24, 2010 - 2:36:20 PM


Files produced by the author(s)


  • HAL Id : inria-00292870, version 7


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⟩



Record views


Files downloads