{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:34:10Z","timestamp":1773653650837,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540600459","type":"print"},{"value":"9783540494133","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_45","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:36:20Z","timestamp":1330277780000},"page":"127-140","source":"Crossref","is-referenced-by-count":26,"title":["Safety property verification of Esterel programs and applications to telecommunications software"],"prefix":"10.1007","author":[{"given":"Lalita Jategaonkar","family":"Jagadeesan","sequence":"first","affiliation":[]},{"given":"Carlos","family":"Puchol","sequence":"additional","affiliation":[]},{"given":"James E.","family":"Olnhausen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"11_CR1","unstructured":"AGEL workshop manual version 3.0, 1989. Produced by ILOG."},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Proc. ACM Symp. on Principles of Distributed Computing, 1991.","DOI":"10.1145\/112600.112613"},{"key":"11_CR3","unstructured":"R. Alur and T. Henzinger. Time for logic. ACM SIGACT News, 22(3), 1991."},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"M. Ardis, John A. Chaves, L. Jagadeesan, P. Mataga, C. Puchol, M. Staskauskas, and J. Von Olnhausen. A framework for evaluating specification methods for reactive systems. In Proc. 17th Intl. Conf. on Software Engineering, April 1995.","DOI":"10.1145\/225014.225029"},{"key":"11_CR5","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"G. Berry and G. Gonthier. The ESTEREL synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19:87\u2013152, 1992.","journal-title":"Science of Computer Programming"},{"key":"11_CR6","unstructured":"A. Bouajjani, J.C. Fernandez, and N. Halbwachs. On the verification of safety properties, 1994. Draft."},{"issue":"2","key":"11_CR7","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2):244\u2013263, 1986.","journal-title":"ACM TOPLAS"},{"key":"11_CR8","doi-asserted-by":"crossref","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data-flow programming language LUSTRE. Proceedings of the IEEE, 79:1305\u20131320, 1991.","journal-title":"Proceedings of the IEEE"},{"issue":"9","key":"11_CR9","doi-asserted-by":"crossref","first-page":"785","DOI":"10.1109\/32.159839","volume":"18","author":"N. Halbwachs","year":"1992","unstructured":"N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE. Transactions on Software Engineering, 18(9):785\u2013793, 1992.","journal-title":"Transactions on Software Engineering"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, D. Pilaud, F. Ouabdesselam, and A.C. Glory. Specifying, programming and verifying reactive systems, using a synchronous declarative language. In Workshop on Automatic Verification Methods for Finite State Systems, LNCS Vol. 407, 1989.","DOI":"10.1007\/3-540-52148-8_18"},{"issue":"6","key":"11_CR11","doi-asserted-by":"crossref","first-page":"1385","DOI":"10.1002\/j.1538-7305.1985.tb00280.x","volume":"64","author":"G. Haugk","year":"1985","unstructured":"G. Haugk, F.M. Lax, R.D. Royer, and J.R. Williams. The 5ESS(TM) switching system: Maintenance capabilities. AT&T Tech. Journal, 64(6 part 2): 1385\u20131416, Jul\u2013Aug 1985.","journal-title":"AT&T Tech. Journal"},{"key":"11_CR12","unstructured":"C. Heitmeyer, R.D. Jeffords, and B. Labaw. A benchmark for comparing different approaches for specifying and verifying real-time systems. In Proc. 10th International Workshop on Real-Time Operating Systems and Software, May 1993."},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"L.J. Jagadeesan, C. Puchol, and J.E. Von Olnhausen. A formal approach to reactive systems software: A telecommunications application in Esterel. In Proc. Workshop on Industrialstrength Formal Spec. Techniques, April 1995.","DOI":"10.1109\/WIFT.1995.515485"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"O Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specifications. In ACM Symposium on Priciples of Programming Languages, pages 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Conference on Logics of Programs, 1985.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"6","key":"11_CR17","doi-asserted-by":"crossref","first-page":"1305","DOI":"10.1002\/j.1538-7305.1985.tb00276.x","volume":"64","author":"K.E. Martersteck","year":"1985","unstructured":"K.E. Martersteck and A.E. Spencer. Introduction to the 5ESS(TM) switching system. AT&T Tech. Journal, 64(6 part 2):1305\u20131314, Jul\u2013Aug 1985.","journal-title":"AT&T Tech. Journal"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"D. Pilaud and N. Halbwachs. From a synchronous declarative language to a temporal logic dealing with multi-form time. In Symposium on Formal Techniques in Real-Time and Fault-Tolerant Techniques, LNCS Vol. 331, 1988.","DOI":"10.1007\/3-540-50302-1_5"},{"key":"11_CR19","volume-title":"Technical Report UTCS-TR95-05","author":"C. Puchol","year":"1995","unstructured":"C. Puchol. A solution to the generalized railroad crossing problem in Esterel. Technical Report UTCS-TR95-05, Dept. of Com. Sci., Univ. of Texas at Austin, Feb 1995."},{"key":"11_CR20","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. LICS, pages 332\u2013339, 1986."},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"P. Wolper, M.Y. Vardi, and A.P. Sistla. Reasoning about infinite computation paths. In IEEE Symposium on Foundations of Computer Science, pages 185\u2013194, 1983.","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_45.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:28:51Z","timestamp":1605648531000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}