Title:
Automatic Verification of a Turbogas Control System
with the Murphi Verifier

Authors:
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, 
Michele Minichino, Ester Ciancamerla, Andrea Parisse,
Enrico Tronci, Marisa Venturini Zilli


Conference:
Proceedings of: 6th International Workshop
"Hybrid Systems: Computation and Control" (HSCC) 
April 2003, Prague, Czech Republic, LNCS 2623, Springer-Verlag


Abstract

Automatic analysis of {\em 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
{\em Turbogas Control System}  (TCS) using an extended version of
the Mur$\varphi$ verifier.
TCS is the heart of {\em ICARO}, 
a 2MW {\em 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$\varphi$ verifier by importing the C language 
{\tt long double} type ({\em finite precision real numbers}) into it.

We give experimental results on running our extended Mur$\varphi$
on our TCS model.
For example using Mur$\varphi$ we were able to compute an admissible 
range of values for the variation speed of the {\em user demand} of 
electric power to the turbogas.