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.
Type de document :
Communication dans un congrès
NFM 2009 : The First NASA Formal Methods Symposium, Apr 2009, Moffett Field, CA, United States. 2009
Liste complète des métadonnées

https://hal.inria.fr/hal-00788418
Contributeur : Ist Rennes <>
Soumis le : jeudi 14 février 2013 - 14:10:42
Dernière modification le : mercredi 16 mai 2018 - 11:23:03

Identifiants

  • HAL Id : hal-00788418, version 1

Citation

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. 2009. 〈hal-00788418〉

Partager

Métriques

Consultations de la notice

322