%0 Conference Proceedings
%T Automatic Verification of a Turbogas Control System with the Mur$\varphi$ Verifier
%A Della Penna, Giuseppe
%A Intrigila, Benedetto
%A Melatti, Igor
%A Minichino, Michele
%A Ciancamerla, Ester
%A Parisse, Andrea
%A Tronci, Enrico
%A Venturini Zilli, Marisa
%Y Maler, O.
%Y Pnueli, A.
%S Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings
%S Lecture Notes in Computer Science
%D 2003
%V 2623
%I Springer
%@ 3-540-00913-2
%F DellaPenna_etal2003
%O exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=88), last updated on Thu, 22 Nov 2012 14:59:18 +0100
%X 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.
%R 10.1007/3-540-36580-X
%U http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2003.pdf
%U https://doi.org/10.1007/3-540-36580-X
%P 141-155