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

G Della Penna, B Intrigila, I Melatti, M Minichino… - … and Control: 6th …, 2003 - Springer
G Della Penna, B Intrigila, I Melatti, M Minichino, E Ciancamerla, A Parisse, E Tronci
Hybrid Systems: Computation and Control: 6th International Workshop, HSCC 2003 …, 2003Springer
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 …
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
以上显示的是最相近的搜索结果。 查看全部搜索结果