Automatic verification of a turbogas control system with the Murφ verifier

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φ 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φ verifier by importing the C language long double type (finite precision real numbers) into it. We give experimental results on running our extended Murφ on our TCS model. For example using Murφ we were able to compute an admissible range of values for the variation speed of the user demand of electric power to the turbogas. © Springer-Verlag Berlin Heidelberg 2003.