The Steam Boiler Controller Problem in ESTEREL and its Verification by Means of Symbolic Analysis

Michel Bourdellès 1
1 MEIJE - Concurrency, Synchronization and Real-time Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We describe the use of the verification tools XEVE and FC2SYMBMIN on the ESTEREL encoding of a Steam Boiler controller proposed by J.R. Abial. XEVE is a verification tool set dedicated to the analysis of synchronous reactive systems in the form of boolean equations, using the symbolic representation of BDDs for implicit state representation. FC2SYMBMIN is a latter addition to this toolset, and allows verification after reduction and abstraction with respect to bisimulation of explicit finite state machines with a symbolic treatment (using BDDs again) of input event predicates. This specific representation triggers new algorithmic issues in the computation of bisimulation classes. We demonstrate the power of FC2SYMBMIN in terms of reduction of states, but also in terms of reduction of transitions for which the gain is often dramatic.
Type de document :
Rapport
RR-3285, INRIA. 1997
Liste complète des métadonnées

https://hal.inria.fr/inria-00073403
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:43:07
Dernière modification le : samedi 27 janvier 2018 - 01:31:29
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:45:26

Fichiers

Identifiants

  • HAL Id : inria-00073403, version 1

Collections

Citation

Michel Bourdellès. The Steam Boiler Controller Problem in ESTEREL and its Verification by Means of Symbolic Analysis. RR-3285, INRIA. 1997. 〈inria-00073403〉

Partager

Métriques

Consultations de la notice

112

Téléchargements de fichiers

185