The Steam Boiler Controller Problem in Signal-Coq

Mickaël Kerboeuf 1 David Nowak 1 Jean-Pierre Talpin 1
1 EP-ATR - Environnement de programmation d'applications temps réel
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : Among the various formalisms for the design of reactive systems, the SIGNAL-CO- Q formal approach, i.e. the combined use of the synchronous dataflow language SIGNAL and the proof assistant COQ, seems to be especially suited and practical. Indeed, the deterministic concurrency implied by the synchronous model on which SIGNAL is founded strongly simplifies the specification and the verification of such systems. Moreover, COQ is not limited to some kind of properties and so, its use enables to disregard what can be checked during the specification stage. In this article, we underline the various features of this SIGNAL-COQ formal approach with a large scale case study, namely the Steam Boiler problem.
Type de document :
Rapport
[Research Report] RR-3773, INRIA. 1999
Liste complète des métadonnées

https://hal.inria.fr/inria-00072888
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 11:11:05
Dernière modification le : mercredi 16 mai 2018 - 11:23:02
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:26:49

Fichiers

Identifiants

  • HAL Id : inria-00072888, version 1

Citation

Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin. The Steam Boiler Controller Problem in Signal-Coq. [Research Report] RR-3773, INRIA. 1999. 〈inria-00072888〉

Partager

Métriques

Consultations de la notice

159

Téléchargements de fichiers

202