Michel Bourdellès
May 16, 1997
We describe the use of the verification tools XEVE and FC2SYMBMIN on the ESTEREL encoding of a Steam Boiler controller.
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, for the 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.
the Steam Boiler problem proposed by J.R Abrial is an interesting problem as, while mostly control-dominated, it includes simple data and value thresholds, calling again for symbolic treatment of behaviours.
We demonstrate the power of FC2SYMBMIN in terms of reduction of states, but also in terms of transitions for which the gain is often dramatic.