Publication interne
Les présents exposés écrits et oraux ainsi que tous les éléments qu'ils comportent, font l'objet d'une protection par le droit d'auteur.
PI 1266 : The Steam Boiler Controller Problem in Signal-Coq
Mickaël Kerboeuf , David Nowak , Jean-Pierre Talpin
01 Octobre 1999
59 pages
Langue: Anglais
Equipe(s): EP-ATR
Mots-clés: Systèmes réactifs, modèle synchrone, vérification, model-checking, assistant de preuve, co-induction
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'assistant de preuve Coq, semble être particulièrement adaptée. En effet, la concurrence 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.