TY - CONF AU - Della Penna, Giuseppe AU - Intrigila, Benedetto AU - Melatti, Igor AU - Minichino, Michele AU - Ciancamerla, Ester AU - Parisse, Andrea AU - Tronci, Enrico AU - Venturini Zilli, Marisa ED - Maler, O. ED - Pnueli, A. PY - 2003 DA - 2003// TI - Automatic Verification of a Turbogas Control System with the Mur$\varphi$ Verifier BT - Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings T3 - Lecture Notes in Computer Science SP - 141 EP - 155 VL - 2623 PB - Springer 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. SN - 3-540-00913-2 L1 - http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2003.pdf UR - https://doi.org/10.1007/3-540-36580-X DO - 10.1007/3-540-36580-X N1 - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=88), last updated on Thu, 22 Nov 2012 14:59:18 +0100 ID - DellaPenna_etal2003 ER -