Skip to Main content Skip to Navigation
Reports

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
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/inria-00292870
Contributor : Yann Glouche <>
Submitted on : Tuesday, January 13, 2009 - 3:48:07 PM
Last modification on : Tuesday, June 15, 2021 - 4:27:00 PM
Long-term archiving on: : Friday, September 24, 2010 - 2:36:20 PM

Files

RR-6570.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

518

Files downloads

191