HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 12:43:07 PM
Last modification on : Friday, February 4, 2022 - 3:16:11 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:45:26 PM


  • HAL Id : inria-00073403, version 1



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



Record views


Files downloads