Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00073403
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 12:43:07 PM
Last modification on : Saturday, January 27, 2018 - 1:31:29 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:45:26 PM

Identifiers

  • 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⟩

Share

Metrics

Record views

134

Files downloads

225