@InProceedings{DellaPenna_etal2003,
author="Della Penna, Giuseppe
and Intrigila, Benedetto
and Melatti, Igor
and Minichino, Michele
and Ciancamerla, Ester
and Parisse, Andrea
and Tronci, Enrico
and Venturini Zilli, Marisa",
editor="Maler, O.
and Pnueli, A.",
title="Automatic Verification of a Turbogas Control System with the Mur{\$}{\backslash}varphi{\$} Verifier",
booktitle="Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings",
series="Lecture Notes in Computer Science",
year="2003",
publisher="Springer",
volume="2623",
pages="141--155",
abstract="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{\$}{\backslash}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{\$}{\backslash}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{\$}{\backslash}varphi{\$} on our TCS model. For example using Mur{\$}{\backslash}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.",
optnote="exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=88), last updated on Thu, 22 Nov 2012 14:59:18 +0100",
issn="3-540-00913-2",
doi="10.1007/3-540-36580-X",
opturl="https://doi.org/10.1007/3-540-36580-X",
file=":http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2003.pdf:PDF"
}