The Steam Boiler Controller Problem in ESTEREL and its Verification by Means of Symbolic Analysis
Michel Bourdellès · 1997
: We describe the use of the verication tools xeve and fc2symbmin on the esterel encoding of a Steam Boiler controller proposed by J.R. Abial. xeve is a verication 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 verication after reduction and abstraction with respect to bisimulation of explicit nite state machines with a symbolic treatment (using BDDs again) of input event predicates. This specic 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. Key-words: Synchronous reactive systems, symbolic bisimulation, verication by observer (R#sum# : tsvp) Unit de recherche INRIA Sophia Antipolis 2004 route de...