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

Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Michele Minichino, Ester Ciancamerla, Andrea Parisse, Enrico Tronci, Marisa Venturini Zilli

Research output: Contribution to journalArticle

18 Citations (Scopus)


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.
Original languageEnglish
Pages (from-to)141 - 155
Number of pages15
JournalLecture Notes in Computer Science
Publication statusPublished - 2003


All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Della Penna, G., Intrigila, B., Melatti, I., Minichino, M., Ciancamerla, E., Parisse, A., ... Zilli, M. V. (2003). Automatic verification of a turbogas control system with the Murφ verifier. Lecture Notes in Computer Science, 2623, 141 - 155.