{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:46:51Z","timestamp":1725497211833},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540009139"},{"type":"electronic","value":"9783540365808"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36580-x_13","type":"book-chapter","created":{"date-parts":[[2007,12,9]],"date-time":"2007-12-09T12:13:36Z","timestamp":1197202416000},"page":"141-155","source":"Crossref","is-referenced-by-count":11,"title":["Automatic Verification of a Turbogas Control System with the Mur\u03c6 Verifier"],"prefix":"10.1007","author":[{"given":"Giuseppe","family":"Della Penna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benedetto","family":"Intrigila","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Melatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michele","family":"Minichino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ester","family":"Ciancamerla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Parisse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marisa","family":"Venturini Zilli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,3,14]]},"reference":[{"key":"13_CR1","unstructured":"url: http:\/\/www.eecs.berkeley.edu\/~tah\/HyTech ."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Trans. on Software Engineering, 22, 1996.","DOI":"10.1109\/32.489079"},{"key":"13_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of 21st International Conference on \u201dComputer Safety, Reliability and Security\u201d (SAFECOMP)","author":"A. Bobbio","year":"2002","unstructured":"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 \u201dComputer Safety, Reliability and Security\u201d (SAFECOMP), LNCS, Catania, Italy, Sept 2002. Springer."},{"key":"13_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of 21st International Conference on \u201cComputer Safety, Reliability and Security\u201d (SAFECOMP)","author":"A. Bobbio","year":"2002","unstructured":"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 \u201cComputer Safety, Reliability and Security\u201d (SAFECOMP), LNCS, Catania, Italy, Sept 2002. Springer."},{"key":"13_CR5","unstructured":"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."},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8), Aug 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"13_CR7","unstructured":"url: http:\/\/www.dsi.unirom1.it\/~tronci\/cached.murphi.html"},{"issue":"6","key":"13_CR8","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1016\/0041-5553(68)90115-8","volume":"8","author":"N. V. Chernikova","year":"1968","unstructured":"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\u2013293, 1968.","journal-title":"USSR Computational Mathematics and Mathematical Physics"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"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\u20135, 1992.","DOI":"10.1109\/ICCD.1992.276232"},{"key":"13_CR10","unstructured":"ENEA. Proprietary ICARO Documentation."},{"key":"13_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Proc. of: Computer Aided Verification (CAV)","author":"N. Halbwachs","year":"1993","unstructured":"N. Halbwachs. Delay analysis in synchronous programs. In Proc. of: Computer Aided Verification (CAV), number 697 in LNCS, pages 333\u2013346. Springer, 1993."},{"key":"13_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-58485-4_43","volume-title":"Proc. of: Static Analysis Symposium (SAS)","author":"N. Halbwachs","year":"1994","unstructured":"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\u2013237. Springer, 1994."},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"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\u201365. IEEE, 1995.","DOI":"10.1109\/REAL.1995.495196"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1, 1997.","DOI":"10.1007\/s100090050008"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"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\u2013282, 1994.","DOI":"10.1145\/196244.196377"},{"issue":"11","key":"13_CR16","first-page":"1356","volume":"10","author":"R.P. Kurshan","year":"1991","unstructured":"R.P. Kurshan and K.L. McMillan. Analysis of digital circuits through symbolic reduction. IEEECAD, 10(11):1356\u20131371, November 1991.","journal-title":"IEEECAD"},{"key":"13_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/3-540-63166-6_47","volume-title":"CAV97","author":"K. G. Larsen","year":"1997","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal: Status and developments. In Orna Grumberg, editor, CAV97, number 1254 in LNCS, pages 456\u2013459. Springer-Verlag, Jun 1997."},{"key":"13_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"K. L. McMillan","year":"1993","unstructured":"K. L. McMillan. Symbolic model checking. Kluwer Academic Publishers, Massachusetts, 1993."},{"key":"13_CR19","unstructured":"url: http:\/\/\/sprout.stanford.edu\/dill\/murphi.html ."},{"key":"13_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of 4th International Conference on \u201cFormal Methods in Computer Aided Verification\u201d (FMCAD)","author":"G. Della Penna","year":"2002","unstructured":"G. Della Penna, B. Intrigila, E. Tronci, and M. Venturini Zilli. Exploiting transition locality in the disk based mur\u03c6 verifier. In Proc. of 4th International Conference on \u201cFormal Methods in Computer Aided Verification\u201d (FMCAD), LNCS, Portland, Oregon, USA, Nov 2002. Springer."},{"key":"13_CR21","unstructured":"url: http:\/\/www.cs.cmu.edu\/~modelcheck\/ ."},{"key":"13_CR22","unstructured":"url: http:\/\/netlib.bell-labs.com\/netlib\/spin\/whatispin.html ."},{"key":"13_CR23","series-title":"Lect Notes Comput Sci","volume-title":"IFIP WG 10.5 Advanced Research Working Conference on: Correct Hardware Design and Verification Methods (CHARME)","author":"E. Tronci","year":"2000","unstructured":"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."},{"key":"13_CR24","unstructured":"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."},{"key":"13_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/BFb0014731","volume-title":"Hybrid and Real-Time Systems","author":"A. L. Turk","year":"1997","unstructured":"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\u2013272. Springer, 1997."},{"key":"13_CR26","unstructured":"url: http:\/\/www.docs.uu.se\/docs\/rtmv\/uppaal\/"}],"container-title":["Lecture Notes in Computer Science","Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36580-X_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T20:16:33Z","timestamp":1557087393000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36580-X_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540009139","9783540365808"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-36580-x_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}