Kerboeuf, Mickaël
- Nowak, David
- Talpin, Jean-Pierre
Rapport de recherche de l'INRIA -
Rennes ,
Equipe : EPATR
59 pages - Octobre 1999 - Document en anglais
Titre français : Le problème du steam-boiler en Signal-Coq
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.
Résumé : Parmi les différents formalismes permettant la conception des systèmes réactifs, l'approche formelle SIGNAL-COQ, i.e. l'utilisation combinée du langage de programmation synchrone à flot de données SIGNAL et de l'assista- nt de preuve COQ, semble être particulièrement adaptée. En effet, la concurren- ce déterministe induite par le modèle synchrone sur lequel SIGNAL est fondé simplifie fortement la spécification et la vérification de tels systèmes. En outre, COQ n'est pas limité à un certain type de propriétés et ainsi, son utilisation permet de faire abstraction de ce qui peut être vérifié pendant la phase de spécification. Dans ce document, nous soulignons les différents aspects de cette approche formelle SIGNAL-COQ à l'aide d'une étude de cas issue de l'industrie, à savoir le problème du steam boiler.
Key-Words : REACTIVE SYSTEMS / SYNCHRONOUS MODEL / VERIFICATION / MODEL CHECKING / PROOF
ASSISTANT / CO-INDUCTION
Mots-clés : SYSTEMES REACTIFS / MODELE SYNCHRONE / VERIFICATION / MODEL-CHECKING /
ASSISTANT DE PREUVE / CO-INDUCTION
