A Boolean Algebra of Contracts for Assume-guarantee Reasoning

Contract-based design is an expressive paradigm for a modular and compositional specification 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: 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 a structure of contracts that is a Heyting algebra.

• Type: Journal
• Year: 2010
• Where: ENTCS
• Authors: Yann Glouche, Paul Le Guernic, Jean-Pierre Talpin, Thierry Gautier
• Keywords: Design, ENTCS 2010, Expressive Paradigm, Industrial Computer-aided Design