Skip to Main content Skip to Navigation
Conference papers

A module language for typing by contracts

Yann Glouche 1 Thierry Gautier 1 Paul Le Guernic 1 Jean-Pierre Talpin 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 modular and compositional specification of programs. It is becoming a fundamental concept in some computer-aided design tools for embedded system design. In this paper, we elaborate foundations for contract-based embedded system design by proposing a general-purpose module language based on a Boolean algebra allowing to define contracts. In this framework, contracts are used to negociate the correctness of assumptions made on the definition of a component at the point where it is used and provides guarantees to its environment. We illustrate this presentation with the specification of a simplified 4-stroke engine model.
Document type :
Conference papers
Complete list of metadata
Contributor : Ist Rennes <>
Submitted on : Thursday, February 14, 2013 - 2:10:42 PM
Last modification on : Tuesday, June 15, 2021 - 4:26:54 PM


  • HAL Id : hal-00788418, version 1


Yann Glouche, Thierry Gautier, Paul Le Guernic, Jean-Pierre Talpin. A module language for typing by contracts. NFM 2009 : The First NASA Formal Methods Symposium, Apr 2009, Moffett Field, CA, United States. ⟨hal-00788418⟩



Record views