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.
This research has been partially supported by MURST projects MEFISTO and SAHARA
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Trans. on Software Engineering, 22, 1996.
A. Bobbio, E. Ciancamerla, G. Franceschinis, R. Gaeta, M. Minichino, and L. Portinale. Methods of increasing modelling power for safety analysis, applied to a turbine digital control system. In Proc. of 21st International Conference on ”Computer Safety, Reliability and Security” (SAFECOMP), LNCS, Catania, Italy, Sept 2002. Springer.
A. Bobbio, E. Ciancamerla, M. Gribaudo, A. Horvath, M. Minichino, and E. Tronci. Model checking based on fluid petri nets for the temperature control system of the icaro co-generative plant. In Proc. of 21st International Conference on “Computer Safety, Reliability and Security” (SAFECOMP), LNCS, Catania, Italy, Sept 2002. Springer.
A. Bobbio, S. Bologna, M. Minichino, E. Ciancamerla, P. Incalcaterra, C. Kropp, and E. Tronci. Advanced tecniques for safety analysis applied to the gas turbine control system of icaro co generative plant. In Proc. of X Convegno TESEC, Genova, Italy, June 2001.
R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8), Aug 1986.
N. V. Chernikova. Algorithm for discovering the set of all solutions of a linear programming problem. USSR Computational Mathematics and Mathematical Physics, 8(6):282–293, 1968.
D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522–5, 1992.
ENEA. Proprietary ICARO Documentation.
N. Halbwachs. Delay analysis in synchronous programs. In Proc. of: Computer Aided Verification (CAV), number 697 in LNCS, pages 333–346. Springer, 1993.
N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximation. In Proc. of: Static Analysis Symposium (SAS), number 864 in LNCS, pages 223–237. Springer, 1994.
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: The next generation. In Proc. of the 16th Annual IEEE Real-time Systems Symposium (RTSS), pages 56–65. IEEE, 1995.
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1, 1997.
A. J. Hu, G. York, and D. L. Dill. New techniques for efficient verification with implicitily conjoined bdds. In 31st IEEE Design Automation Conference, pages 276–282, 1994.
R.P. Kurshan and K.L. McMillan. Analysis of digital circuits through symbolic reduction. IEEECAD, 10(11):1356–1371, November 1991.
Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal: Status and developments. In Orna Grumberg, editor, CAV97, number 1254 in LNCS, pages 456–459. Springer-Verlag, Jun 1997.
K. L. McMillan. Symbolic model checking. Kluwer Academic Publishers, Massachusetts, 1993.
G. Della Penna, B. Intrigila, E. Tronci, and M. Venturini Zilli. Exploiting transition locality in the disk based murφ verifier. In Proc. of 4th International Conference on “Formal Methods in Computer Aided Verification” (FMCAD), LNCS, Portland, Oregon, USA, Nov 2002. Springer.
url: http://netlib.bell-labs.com/netlib/spin/whatispin.html.
E. Tronci, G. Della Penna, B. Intrigila, and M. Venturini Zilli. Exploiting transition locality in automatic verification. In IFIP WG 10.5 Advanced Research Working Conference on: Correct Hardware Design and Verification Methods (CHARME). LNCS, Springer, Sept 2001.
E. Tronci, G. Della Penna, B. Intrigila, and M. Venturini Zilli. A probabilistic approach to space-time trading in automatic verification of concurrent systems. In Proc. of 8th IEEE Asia-Pacific Software Engineering Conference (APSEC), Macau SAR, China, Dec 2001. IEEE Computer Society Press.
A. L. Turk, S. T. Probst, and G. J. Powers. Verification of real-time chemical processing systems. In Hybrid and Real-Time Systems, number 1201 in LNCS, pages 259–272. Springer, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Della Penna, G. et al. (2003). Automatic Verification of a Turbogas Control System with the Murφ Verifier. In: Maler, O., Pnueli, A. (eds) Hybrid Systems: Computation and Control. HSCC 2003. Lecture Notes in Computer Science, vol 2623. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36580-X_13
Download citation
DOI: https://doi.org/10.1007/3-540-36580-X_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00913-9
Online ISBN: 978-3-540-36580-8
eBook Packages: Springer Book Archive