Automatic analysis of
Hybrid Systems poses formidable challenges both from a modeling as well as from a verification point of view. We present a case study on
automatic verification of a
Turbogas Control System (TCS) using an extended version of the Mur. verifier. TCS is the heart of
ICARO, a 2MW
Co-generative Electric Power Plant. For large hybrid systems, as TCS is, the modeling effort accounts for a significant part of the whole verification activity.
In order to ease our modeling effort we extended the Murφ verifier by importing the C language long double type (
finite precision real numbers) into it.
We give experimental results on running our extended Murφon our TCS model. For example using Mur. we were able to compute
an admissible range of values for the variation speed of the user demand of electric power to the turbogas.
This research has been partially supported by MURST projects MEFISTO and SAHARA