A Boolean algebra of contracts for logical assume-guarantee reasoning - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Reports (Research Report) Year : 2008

A Boolean algebra of contracts for logical assume-guarantee reasoning

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.
Fichier principal
Vignette du fichier
RR-6570.pdf (682.25 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00292870 , version 1 (02-07-2008)
inria-00292870 , version 2 (03-07-2008)
inria-00292870 , version 3 (07-07-2008)
inria-00292870 , version 4 (11-07-2008)
inria-00292870 , version 5 (25-07-2008)
inria-00292870 , version 6 (09-10-2008)
inria-00292870 , version 7 (13-01-2009)

Identifiers

  • HAL Id : inria-00292870 , version 5

Cite

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

Collections

INRIA-RRRT
223 View
97 Download

Share

Gmail Facebook X LinkedIn More