{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,15]],"date-time":"2025-07-15T00:01:16Z","timestamp":1752537676220,"version":"3.41.2"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2001,4,1]],"date-time":"2001-04-01T00:00:00Z","timestamp":986083200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,4,1]],"date-time":"2001-04-01T00:00:00Z","timestamp":986083200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Design Automation for Embedded Systems"],"published-print":{"date-parts":[[2001,4]]},"DOI":"10.1023\/a:1011237030847","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T04:18:21Z","timestamp":1040617101000},"page":"151-175","source":"Crossref","is-referenced-by-count":0,"title":["Specification and Validation of Embedded Systems using LUSTRE and ARGOS. Case Study: The Automatic Headlight Leveling System"],"prefix":"10.1007","volume":"6","author":[{"given":"Rainer","family":"Gmehlich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"9","key":"354142_CR1","doi-asserted-by":"crossref","first-page":"1270","DOI":"10.1109\/5.97297","volume":"79","author":"A. Benveniste","year":"1991","unstructured":"A. Benveniste and G. Berry. The synchronous approach to reactive and real-time systems. Proceedings of the IEEE, 79(9):1270\u20131282, September 1991.","journal-title":"Proceedings of the IEEE"},{"key":"354142_CR2","unstructured":"R. Budde and A. Merceron. A generator of boolean acceptors for safety properties. To appear."},{"key":"354142_CR3","doi-asserted-by":"crossref","unstructured":"R. Budde, A. Merceron, and K.-H. Sylla. Formal verification as a design tool\u2014the transponder lock example. In 15th International Conference on Computer Safety, Reliability and Security, October 1996.","DOI":"10.1007\/978-1-4471-0937-2_6"},{"key":"354142_CR4","series-title":"Technical report","volume-title":"se the design and programming language embedded eifel (se version 1.1)","author":"R. Budde","year":"1998","unstructured":"Reinhard Budde. se the design and programming language embedded eifel (se version 1.1). Technical report, GMD-SET-EES, Schlo\u00df Birlinghoven, St. Augustin, April 1998."},{"key":"354142_CR5","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking 1020 and beyond. Information and Computation, 98:142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"354142_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications: A practical approach. In Conference record of the 10th ACM Symposium on Principles of Programming Languages (POPL), Austin, TX, 1983, pages 117\u2013126.","DOI":"10.1145\/567067.567080"},{"key":"354142_CR7","unstructured":"E. P\u00e4rt-Enander and A. Sj7#x00F6;berg. The MATLAB 5 Handbook. Addison-Wesley, 1999."},{"issue":"9","key":"354142_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(9):1305\u20131319, September 1991.","journal-title":"Proceedings of the IEEE"},{"key":"354142_CR9","unstructured":"N. Halbwachs, J.-C. Fernandez, and A. Bouajjanni. An executable temporal logic to express safety properties and its connection with the language lustre. In Sixth International Symp. on Lucid and Intensional Programming, ISLIP' 93, April 1993."},{"key":"354142_CR10","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the verification of reactive systems. In T. Rus, G. Scollo, M. Nivat, and C. Rattray, editors, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST 93, Twente, June 1993. Workshop in Computing, Springer Verlag.","DOI":"10.1007\/978-1-4471-3227-1_8"},{"key":"354142_CR11","doi-asserted-by":"crossref","unstructured":"N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer Academic Press, 1993.","DOI":"10.1007\/978-1-4757-2231-4"},{"issue":"9","key":"354142_CR12","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. IEEE Transactions on Software Engineering, 18(9):785\u2013793, September 1992.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"354142_CR13","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: Avisual formalism for complex system. Science of Computer Programming, 8(3): 231\u2013274, 1987.","journal-title":"Science of Computer Programming"},{"issue":"4","key":"354142_CR14","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politiand, R. Sherman, and A. Shtull-Trauring. Statemate: a working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering, 16(4):403\u2013413, April 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"354142_CR15","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/978-3-642-82453-1_17","volume-title":"Logics and Models of Concurrent Systems","author":"D. Harel","year":"1985","unstructured":"D. Harel and A. Pnueli. On the development of reactive systems. In K. R. Apt, editor, Logics and Models of Concurrent Systems, Springer, New York, 1985, pages 477\u2013498."},{"key":"354142_CR16","unstructured":"L. Holenderski and A. Poigne. Synchronie workbench light. http:\/\/set.gmd.de\/SET\/ees_f.html, 1997."},{"key":"354142_CR17","first-page":"47","volume":"22","author":"W.-H. Hucho","year":"1992","unstructured":"W.-H. Hucho. Zweimal leuchtweitenregelung. Automobil Revue, 22:47\u201349, Mai 1992.","journal-title":"Automobil Revue"},{"key":"354142_CR18","doi-asserted-by":"crossref","unstructured":"L. J. Jagadeesan, C. Puchol, and J. E. Von Olnhausen. Safety property verification of reactive systems. In P. Wolper, editor, Computer aided verification, in Lecture Notes in Computer Science, Springer Verlag, 1995, volume 939, pages 127\u2013140.","DOI":"10.1007\/3-540-60045-0_45"},{"key":"354142_CR19","unstructured":"S. M. MacMenamin and J. F. Palmer. Essential System Analysis. Prentice Hall, 1984."},{"key":"354142_CR20","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"354142_CR21","volume-title":"Workshop on Automatic Verification Methods for Finite State Systems","author":"F. Maraninchi","year":"1989","unstructured":"F. Maraninchi. Argonaute, graphical description, semantics and verification of reactive systems by using a process algebra. In Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, Springer Verlag, Grenoble, jun 1989."},{"key":"354142_CR22","unstructured":"F. Maraninchi. The argos language: Graphical representation of automata and description of reactive systems. In IEEE Workshop on Visual Languages, oct 1991."},{"key":"354142_CR23","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"354142_CR24","first-page":"2","volume":"1","author":"S. J. Mellor","year":"1985","unstructured":"S. J. Mellor and P. T. Ward. Structured Development for Real-Time Systems, Yourdon Press, 1985, volumes 1, 2, 3.","journal-title":"Structured Development for Real-Time Systems"},{"key":"354142_CR25","unstructured":"MSR. Final documentation of the project msr. Technical report, MSR, Mar 1996."},{"key":"354142_CR26","doi-asserted-by":"crossref","unstructured":"M. Muellerburg, L. Holenderski, O. Maffeis, A. Merceron, and M. Morley. Systematic testing and formal verification to validate reactive programs. Software Quality Journal, pages 287\u2013307, 1995.","DOI":"10.1007\/BF00402649"},{"key":"354142_CR27","unstructured":"A. Poigne, M. Morley, O. Maffeis, L. Holenderski, and R. Budde. The synchronous approach to designing reactive systems. In Formal Methods in System Design. Kluwer Academic Publishers, 1996."},{"key":"354142_CR28","volume-title":"D\u00e9finition et r\u00e9alisation d'un outil de v\u00e9rification formelle de programmes Lustre: Le sys\u00e9me Lesar","author":"C. Ratel","year":"1992","unstructured":"C. Ratel. D\u00e9finition et r\u00e9alisation d'un outil de v\u00e9rification formelle de programmes Lustre: Le sys\u00e9me Lesar. PhD thesis, Universit\u00e9 Joseph Fourrier, Grenoble, June 1992."},{"key":"354142_CR29","unstructured":"C. Toop. Dynamische leuchtweiteregelung. Automobiltechnische Zeitschrift, 9, 1993."},{"key":"354142_CR30","first-page":"307","volume":"1051","author":"M. Weber","year":"1996","unstructured":"M. Weber. Combining statecharts and Z for the design of safety-critical control systems. In Industrial Benefits and Advances in Formal Methods, LNCS, Springer Verlag, 1996, volume 1051, pages 307\u2013326.","journal-title":"Industrial Benefits and Advances in Formal Methods"}],"container-title":["Design Automation for Embedded Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011237030847.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1011237030847\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011237030847.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,14]],"date-time":"2025-07-14T02:21:33Z","timestamp":1752459693000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1011237030847"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,4]]},"references-count":30,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,4]]}},"alternative-id":["354142"],"URL":"https:\/\/doi.org\/10.1023\/a:1011237030847","relation":{},"ISSN":["0929-5585","1572-8080"],"issn-type":[{"type":"print","value":"0929-5585"},{"type":"electronic","value":"1572-8080"}],"subject":[],"published":{"date-parts":[[2001,4]]}}}