{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:09:15Z","timestamp":1761610155770,"version":"build-2065373602"},"reference-count":26,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2002,6,1]],"date-time":"2002-06-01T00:00:00Z","timestamp":1022889600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,6,1]],"date-time":"2002-06-01T00:00:00Z","timestamp":1022889600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4076,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,6]]},"DOI":"10.1016\/s1571-0661(04)00330-5","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T05:34:35Z","timestamp":1075959275000},"page":"244-256","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Specifying and verifying reactive systems in a multi-language environment"],"prefix":"10.1016","volume":"62","author":[{"given":"Agathe","family":"Merceron","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Monica","family":"M\u00fcllerburg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.Michele","family":"Pinna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"year":"2000","series-title":"\u201cExtreme Programming explained: embrace change\u201d","author":"Beck","key":"10.1016\/S1571-0661(04)00330-5_NEWBIB1"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB2","doi-asserted-by":"crossref","unstructured":"Benveniste A. and G. Berry, The synchronous approach to reactive and realtime systems, Proceedings of the IEEE 79 (1991).","DOI":"10.1109\/5.97297"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB3","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","article-title":"The Esterel synchronous programming language: Design, semantics, implementation","volume":"19","author":"Berry","year":"1992","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB4","unstructured":"Budde, R. and A. Merceron, A generator of boolean acceptors for safety properties, in: 5th Australasian Conf. on Parallel and Real-Time Systems (Part'98), Springer-Verlag, 1998, pp. 45\u201356"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB5","doi-asserted-by":"crossref","unstructured":"Caspi, P., D. Pilaud, N. Halbwachs and J. Plaice, Lustre: a declarative language for programming synchronous systems, in: 14th ACM Conf. on Principles of Programming Languages, ACM Press, 1987, pp. 178\u2013188.","DOI":"10.1145\/41625.41641"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB6","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB7","unstructured":"Esterel homepage, http:\/\/www.esterel.org."},{"year":"1993","series-title":"\u201cSynchronous Programming of Reactive Systems,\u201d","author":"Halbwachs","key":"10.1016\/S1571-0661(04)00330-5_NEWBIB8"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB9","doi-asserted-by":"crossref","unstructured":"Halbwachs N., F. Lagnier and P. Raymond, Synchronous observers and the verification of reactive systems, in: Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, Workshops in Computing, Springer-Verlag, 1993.","DOI":"10.1007\/978-1-4471-3227-1_8"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB10","unstructured":"Kopetz H. and G. Gr\u00fcnsteidl, A time triggered protocol for automotive applications, Research report 16\/92, Institut f\u00fcr Technische Informatik, Technische Universit\u00e4t Wien, Vienna, Austria (1992)."},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB11","doi-asserted-by":"crossref","unstructured":"Kupferman O. and M.Y. Vardi, Modular model checking, in: Proc. Com positionality Workshop, Lecture Notes in Computer Science 1536, Springer-Verlag, 1998.","DOI":"10.1007\/3-540-49213-5_14"},{"year":"1992","series-title":"\u201cThe Temporal Logic of Reactive and Concurrent Systems - Specification,\u201d","author":"Manna","key":"10.1016\/S1571-0661(04)00330-5_NEWBIB12"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB13","unstructured":"Maraninchi F., The Argos language: Graphical representation of auto mata and description of reactive systems, in: IEEE Workshop on Visual Languages, IEEE Society Press, 1991."},{"year":"1993","series-title":"\u201cSymbolic Model Checking,\u201d","author":"McMillan","key":"10.1016\/S1571-0661(04)00330-5_NEWBIB14"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB15","series-title":"6th Australasian Conf. on Parallel and Real-Time Systems (Part'99)","first-page":"367","article-title":"Modular verification of\n\t\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\t\tArgos\n\t\t\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\t programs","author":"Merceron","year":"1999"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB16","unstructured":"Merceron A. and G. Michele Pinna, Refinement and modular verification with observers, in: 1st Asia-Pacific Conference on Quality Software (APAQS 2000), IEEE Society Press, 2000, pp. 104\u2013114."},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB17","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1142\/S0218194001000463","article-title":"Component-based verification is a synchronous setting","volume":"11","author":"Merceron","year":"2001","journal-title":"International Journal of Software Engineering & Knowledge Engineering"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB18","doi-asserted-by":"crossref","unstructured":"Merceron A., M. M\u00fcllerburg and G. Michele Pinna, Verifying a time triggered protocol in a multi language environment, in: Proceedings of Safecomp '98, Lecture Notes in Computer Sciences 1516, Springer-Verlag, 1998, pp. 185\u2013195.","DOI":"10.1007\/3-540-49646-7_14"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB19","unstructured":"Poign\u00e8, A. and L. Holenderski, Boolean automata for implementing ESTEREL, Arbeitspapiere der GMD 964, GMD (1995)."},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB20","doi-asserted-by":"crossref","unstructured":"Poign\u00e9, A. and L. Holenderski, On the combination of synchronous languages, in: Compositionality: The Significant Difference, Lecture Notes in Computer Science 1536, Springer-Verlag, 1999, pp 490 \u2013514.","DOI":"10.1007\/3-540-49213-5_19"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB21","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1023\/A:1008697810328","article-title":"The synchronous approach to designing reactive systems","volume":"12","author":"Poign\u00e9","year":"1998","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB22","unstructured":"SCADE homepage, http:\/\/www.telelogic.com\/products\/scade\/."},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB23","unstructured":"sE homepage, http:\/\/set.gmd.de\/ees\/synchronie\/doc\/lang.html."},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB24","unstructured":"SYNCHRONIE homepage, http:\/\/set.gmd.de\/ees\/synchronie\/swb.html."},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB25","doi-asserted-by":"crossref","unstructured":"The VIS Group, VIS: A system for verification and synthesis, in: Proc. 8th International Conference on Computer Aided Verification, Lecture Notes in Computer Science 1102, Springer-Verlag, 1996, pp. 428\u2013432.","DOI":"10.1007\/3-540-61474-5_95"},{"key":"10.1016\/S1571-0661(04)00330-5_NEWBIB26","unstructured":"v. Hanxleden, R., J. Bohne, L. Lavagno and A. Sangiovanni-Vincentelli, Hardware\/software co-design of a fault-tolerant communication protocol, in: Proc. of the IEEE International Workshop on Embedded Fault-Tolerant Systems, Dallas, 1996."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104003305?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104003305?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:04:38Z","timestamp":1761609878000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104003305"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,6]]},"references-count":26,"alternative-id":["S1571066104003305"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00330-5","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,6]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Specifying and verifying reactive systems in a multi-language environment","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)00330-5","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}