PT Unknown
AU Della Penna, G
   Intrigila, B
   Melatti, I
   Minichino, M
   Ciancamerla, E
   Parisse, A
   Tronci, E
   Venturini Zilli, M
TI Automatic Verification of a Turbogas Control System with the Mur$\varphi$ Verifier
SE Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings
PY 2003
BP 141
EP 155
VL 2623
DI 10.1007/3-540-36580-X
AB 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$\varphi$ 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$\varphi$ verifier by importing the C language long double type (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 user demand of electric power to the turbogas.
ER