{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,13]],"date-time":"2023-01-13T23:54:45Z","timestamp":1673654085869},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,4,10]],"date-time":"2013-04-10T00:00:00Z","timestamp":1365552000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/2.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Embedded Systems"],"published-print":{"date-parts":[[2013,12]]},"DOI":"10.1186\/1687-3963-2013-3","type":"journal-article","created":{"date-parts":[[2013,4,10]],"date-time":"2013-04-10T10:41:55Z","timestamp":1365590515000},"source":"Crossref","is-referenced-by-count":6,"title":["Clock refinement in imperative synchronous languages"],"prefix":"10.1186","volume":"2013","author":[{"given":"Mike","family":"Gem\u00fcnde","sequence":"first","affiliation":[]},{"given":"Jens","family":"Brandt","sequence":"additional","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,4,10]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1109\/JPROC.2002.805826","volume":"91","author":"A Benveniste","year":"2003","unstructured":"Benveniste A, Caspi P, Edwards S, Halbwachs N, Le Guernic P, de Simone R: The synchronous languages twelve years later. Proc. IEEE 2003, 91: 64-83. 10.1109\/JPROC.2002.805826","journal-title":"Proc. IEEE"},{"key":"22_CR2","first-page":"425","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner","author":"G Berry","year":"1998","unstructured":"Berry G: The foundations of Esterel. In Proof, Language and Interaction: Essays in Honour of Robin Milner. Edited by: Tofte M, Plotkin G, Stirling C, Tofte M . MIT Press Cambridge; 1998:425-454."},{"issue":"9","key":"22_CR3","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs N, Caspi P, Raymond P, Pilaud D: The synchronous dataflow programming language LUSTRE. Proc. IEEE 1991,79(9):1305-1320. 10.1109\/5.97300","journal-title":"Proc. IEEE"},{"key":"22_CR4","unstructured":"Schneider K: The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, 2009"},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/BF02811340","volume":"17","author":"G Berry","year":"1992","unstructured":"Berry G: A hardware implementation of pure Esterel. Sadhana 1992, 17: 95-130. 10.1007\/BF02811340","journal-title":"Sadhana"},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/BFb0031993","volume-title":"Real-Time: Theory in Practice vol. 600 of LNCS","author":"F Rocheteau","year":"1992","unstructured":"Rocheteau F, Halbwachs N: Implementing reactive programs on circuits: a hardware implementation of LUSTRE. In Real-Time: Theory in Practice vol. 600 of LNCS. Edited by: Rozenberg G, de Bakker J, Huizing C, de Roever WP, Rozenberg G . Springer Mook, The Netherlands; 1992:195-208."},{"key":"22_CR7","volume-title":"The constructive semantics of pure Esterel","author":"G Berry","year":"1999","unstructured":"Berry G: The constructive semantics of pure Esterel.1999. [\n                    http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.46.2076\n                    \n                  ]"},{"key":"22_CR8","first-page":"205","volume-title":"Distributed and Parallel Embedded Systems (DIPES)","author":"K Schneider","year":"2000","unstructured":"Schneider K: A verified hardware synthesis for Esterel. In Distributed and Parallel Embedded Systems (DIPES). Edited by: Rammig F, Rammig F . Kluwer Schlo\u00df Ehringerfeld; 2000:205-214."},{"key":"22_CR9","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1109\/CSD.2001.981772","volume-title":"Application of Concurrency to System Design (ACSD)","author":"K Schneider","year":"2001","unstructured":"Schneider K: Embedding imperative synchronous languages in interactive theorem provers. In Application of Concurrency to System Design (ACSD). IEEE Computer Society Newcastle Upon Tyne; 2001:143-154."},{"issue":"4","key":"22_CR10","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.entcs.2006.02.028","volume":"153","author":"K Schneider","year":"2006","unstructured":"Schneider K, Brandt J, Schuele T: A verified compiler for synchronous programs with local declarations. Electron. Notes Theor. Comput. Sci. (ENTCS) 2006,153(4):71-97. 10.1016\/j.entcs.2006.02.028","journal-title":"Electron. Notes Theor. Comput. Sci. (ENTCS)"},{"key":"22_CR11","doi-asserted-by":"publisher","unstructured":"Li YT, Malik S: Performance analysis of real-time embedded software. (Kluwer, The Netherlands, 1999)","DOI":"10.1007\/978-1-4615-5131-7"},{"key":"22_CR12","first-page":"10196","volume-title":"Design, Automation and Test in Europe (DATE)","author":"G Logothetis","year":"2003","unstructured":"Logothetis G, Schneider K: Exact high level WCET analysis of synchronous programs by symbolic state space exploration. In Design, Automation and Test in Europe (DATE). IEEE Computer Society Munich; 2003:10196-10203."},{"issue":"4","key":"22_CR13","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/j.entcs.2008.05.011","volume":"203","author":"M Boldt","year":"2008","unstructured":"Boldt M, Traulsen C, von Hanxleden R: Worst case reaction time analysis of concurrent reactive programs. Electron. Notes Theor. Comput. Sci. (ENTCS) 2008,203(4):65-79. 10.1016\/j.entcs.2008.05.011","journal-title":"Electron. Notes Theor. Comput. Sci. (ENTCS)"},{"key":"22_CR14","first-page":"48","volume-title":"Design Automation Conference (DAC)","author":"L Ju","year":"2010","unstructured":"Ju L, Khoa Huynh B, Roychoudhury A, Chakraborty S: Timing analysis of Esterel programs on general purpose multiprocessors. In Design Automation Conference (DAC). Edited by: Sapatnekar S. (ACM Anaheim; 2010:48-51."},{"key":"22_CR15","doi-asserted-by":"publisher","DOI":"10.1145\/1023833.1023859","volume-title":"Causality analysis of synchronous programs with delayed actions","author":"K Schneider","year":"2004","unstructured":"Schneider K, Brandt J, Schuele T: Causality analysis of synchronous programs with delayed actions. 2004."},{"key":"22_CR16","first-page":"59","volume-title":"Languages, Compilers, and Tools for Embedded Systems (LCTES)","author":"B Titzer","year":"2005","unstructured":"Titzer B, Palsberg J: Nonintrusive precision instrumentation of microcontroller software. In Languages, Compilers, and Tools for Embedded Systems (LCTES). Edited by: Gupta R, Paek Y, Gupta R . ACM Chicago, IL; 2005:59-68."},{"key":"22_CR17","first-page":"161","volume-title":"Formal Methods and Models for Codesign (MEMOCODE)","author":"J Brandt","year":"2009","unstructured":"Brandt J, Schneider K: Static data-flow analysis of synchronous programs. In Formal Methods and Models for Codesign (MEMOCODE). Edited by: Bloem R, Schaumont P. IEEE Computer Society Cambridge; 2009:161-170."},{"issue":"9","key":"22_CR18","doi-asserted-by":"publisher","first-page":"1059","DOI":"10.1109\/43.945302","volume":"20","author":"L Carloni","year":"2001","unstructured":"Carloni L, McMillan K, Sangiovanni-Vincentelli A: Theory of latency-insensitive design. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. (T-CAD) 2001,20(9):1059-1076. 10.1109\/43.945302","journal-title":"IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. (T-CAD)"},{"key":"22_CR19","first-page":"657","volume-title":"Design Automation Conference (DAC)","author":"J Cortadella","year":"2006","unstructured":"Cortadella J, Kishinevsky M, Grundmann B: Synthesis of synchronous elastic architectures. In Design Automation Conference (DAC). Edited by: Sentovich E, Sentovich E . ACM San Francisco; 2006:657-662."},{"key":"22_CR20","first-page":"19","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"S Krstic","year":"2006","unstructured":"Krstic S, Cortadella J, Kishinevsky M, O\u2019Leary J: Synchronous elastic networks. In Formal Methods in Computer-Aided Design (FMCAD). Edited by: Manolios P, Gupta A, Manolios P . IEEE Computer Society San Jose; 2006:19-30."},{"key":"22_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2231-4","volume-title":"Synchronous Programming of Reactive Systems","author":"N Halbwachs","year":"1993","unstructured":"Halbwachs N: Synchronous Programming of Reactive Systems. Kluwer, The Netherlands; 1993."},{"issue":"4","key":"22_CR22","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D Harel","year":"1996","unstructured":"Harel D, Naamad A: The STATEMATE semantics of Statecharts. ACM Trans. Softw. Eng. Methodol. (TOSEM) 1996,5(4):293-333. 10.1145\/235321.235322","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"issue":"7","key":"22_CR23","doi-asserted-by":"publisher","first-page":"950","DOI":"10.1109\/43.293952","volume":"13","author":"S Malik","year":"1994","unstructured":"Malik S: Analysis of cycle combinational circuits. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. (T-CAD) 1994,13(7):950-956. 10.1109\/43.293952","journal-title":"IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. (T-CAD)"},{"key":"22_CR24","volume-title":"Euromicro Conference","author":"N Halbwachs","year":"1995","unstructured":"Halbwachs N, Maraninchi F: On the symbolic analysis of combinational loops in circuits and synchronous programs. In Euromicro Conference. IEEE Computer Society Como; 1995."},{"key":"22_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4210-9","volume-title":"Asynchronous Circuits","author":"J Brzozowski","year":"1995","unstructured":"Brzozowski J, Seger CJ: Asynchronous Circuits. Springer, New York; 1995."},{"key":"22_CR26","first-page":"328","volume-title":"European Design Automation Conference (EDAC)","author":"T Shiple","year":"1996","unstructured":"Shiple T, Berry G, Touati H: Constructive analysis of cyclic circuits. In European Design Automation Conference (EDAC). IEEE Computer Society Paris; 1996:328-333."},{"key":"22_CR27","volume-title":"Institut National de Recherche en Informatique et en Automatique (INRIA)","author":"F Boussinot","year":"1998","unstructured":"Boussinot F: SugarCubes implementation of causality. Research Report 3487, Institut National de Recherche en Informatique et en Automatique (INRIA), Sophia Antipolis, France 1998"},{"key":"22_CR28","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1109\/ACSD.2005.24","volume-title":"Application of Concurrency to System Design (ACSD)","author":"K Schneider","year":"2005","unstructured":"Schneider K, Brandt J, Schuele T, Tuerk T: Maximal causality analysis,. In Application of Concurrency to System Design (ACSD). Edited by: Watanabe Y, Desel J, Watanabe Y . IEEE Computer Society Saint-Malo; 2005:106-115."},{"key":"22_CR29","volume-title":"Separate translation of synchronous programs to guarded actions","author":"J Brandt","year":"2011","unstructured":"Brandt J, Schneider K: Separate translation of synchronous programs to guarded actions. Internal Report 382\/11, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany 2011"},{"key":"22_CR30","first-page":"39","volume-title":"Formal Methods and Models for Codesign (MEMOCODE)","author":"O Tardieu","year":"2004","unstructured":"Tardieu O, de Simone R: Curing schizophrenia by program rewriting in Esterel. In Formal Methods and Models for Codesign (MEMOCODE). IEEE Computer Society San Diego; 2004:39-48."},{"key":"22_CR31","first-page":"1","volume-title":"Software and Compilers for Embedded Systems (SCOPES) Volume 320 of ACM International Conference Proceeding Series","author":"J Brandt","year":"2009","unstructured":"Brandt J, Schneider K: Separate compilation for synchronous programs. In Software and Compilers for Embedded Systems (SCOPES) Volume 320 of ACM International Conference Proceeding Series. Edited by: Falk H, Falk H . ACM Nice; 2009:1-10."},{"key":"22_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-9668-0_6","volume-title":"Parallel Program Design","author":"K Chandy","year":"1989","unstructured":"Chandy K, Misra J: Parallel Program Design. Addison-Wesley, Austin; 1989."},{"key":"22_CR33","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer-Aided Verification (CAV), Volume 110 of LNCS","author":"D Dill","year":"1996","unstructured":"Dill D: The Murphi verification system. In Computer-Aided Verification (CAV), Volume 110 of LNCS. Edited by: Henzinger T, Alur R, Henzinger T . Springer New Brunswick; 1996:390-393."},{"key":"22_CR34","volume-title":"The temporal logic of actions","author":"L Lamport","year":"1991","unstructured":"Lamport L: The temporal logic of actions. Technical Report 79 Digital Equipment Cooperation 1991"},{"key":"22_CR35","first-page":"157","volume-title":"Application of Concurrency to System Design (ACSD)","author":"M Gem\u00fcnde","year":"2010","unstructured":"Gem\u00fcnde M, Brandt J, Schneider K: A formal semantics of clock refinement in imperative synchronous languages. In Application of Concurrency to System Design (ACSD). Edited by: Fernandes J, Gomes L, Khomenko V, Fernandes J . IEEE Computer Society Braga; 2010:157-168."},{"key":"22_CR36","volume-title":"A structural approach to operational semantics","author":"G Plotkin","year":"1981","unstructured":"Plotkin G: A structural approach to operational semantics. Technical Report FN-19, DAIMI, Arhus, Denmark 1981"},{"key":"22_CR37","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.entcs.2005.12.012","volume":"148","author":"P Mosses","year":"2006","unstructured":"Mosses P: Formal semantics of programming languages. Electron. Notes Theor. Comput. Sci. (ENTCS) 2006, 148: 41-73. 10.1016\/j.entcs.2005.12.012","journal-title":"Electron. Notes Theor. Comput. Sci. (ENTCS)"},{"key":"22_CR38","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/3-540-15670-4_19","volume-title":"Seminar on Concurrency (CONCUR) Volume 197 of LNCS","author":"G Berry","year":"1985","unstructured":"Berry G, Cosserat L: The Esterel synchronous programming language and its mathematical semantics. In Seminar on Concurrency (CONCUR) Volume 197 of LNCS. Edited by: Brookes S, Roscoe A, Winskel G. Springer Pittsburgh; 1985:389-448."},{"key":"22_CR39","volume-title":"Structural operational semantics for synchronous languages","author":"S Tini","year":"2000","unstructured":"Tini S: Structural operational semantics for synchronous languages. PhD thesis. University of Pisa, Italy, 2000"},{"key":"22_CR40","first-page":"1","volume-title":"Forum on Specification and Design Languages (FDL)","author":"M Gem\u00fcnde","year":"2011","unstructured":"Gem\u00fcnde M, Brandt J, Schneider K: Schizophrenia and causality in the context of refined clocks. In Forum on Specification and Design Languages (FDL). Edited by: Ghenassia O, Morawiec K, Hinderscheit J, Ghenassia O . IEEE Computer Society Oldenburg; 2011:1-8."},{"key":"22_CR41","first-page":"25","volume-title":"High Level Design Validation and Test Workshop (HLDVT)","author":"M Gem\u00fcnde","year":"2011","unstructured":"Gem\u00fcnde M, Brandt J, Schneider K: Causality analysis of synchronous programs with refined clocks. In High Level Design Validation and Test Workshop (HLDVT). IEEE Computer Society; 2011:25-32."},{"key":"22_CR42","first-page":"209","volume-title":"Formal Methods and Models for Codesign (MEMOCODE)","author":"M Gem\u00fcnde","year":"2010","unstructured":"Gem\u00fcnde M, Brandt J, Schneider K: Compilation of imperative synchronous programs with refined clocks. In Formal Methods and Models for Codesign (MEMOCODE). Edited by: Jobstmann B, Carloni L, Jobstmann B . IEEE Computer Society Grenoble; 2010:209-218."},{"key":"22_CR43","volume-title":"A quick guide to Esterel","author":"G Berry","year":"1997","unstructured":"Berry G: A quick guide to Esterel.1997. [\n                    http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.42.2222\n                    \n                  ]"},{"key":"22_CR44","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-44798-9_10","volume-title":"Correct Hardware Design and Verification Methods (CHARME), Volume 2144 of LNCS","author":"G Berry","year":"2001","unstructured":"Berry G, Sentovich E: Correct Hardware Design and Verification Methods (CHARME), Volume 2144 of LNCS. Edited by: Melham T, Margaria T, Melham T . Livingston: Springer; 2001:110-125."},{"key":"22_CR45","first-page":"201","volume-title":"International Parallel and Distributed Processing Symposium (IPDPS), Canc\u00fan","author":"B Rajan","year":"2000","unstructured":"Rajan B, Shyamasundar R: Multiclock ESTEREL: a reactive framework for asynchronous design. In International Parallel and Distributed Processing Symposium (IPDPS), Canc\u00fan. Quintana Roo: IEEE Computer Society; 2000:201-209."},{"key":"22_CR46","first-page":"301","volume-title":"Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\/PSTV)","author":"B Rajan","year":"2000","unstructured":"Rajan B, Shyamasundar R: Modeling distributed embedded systems in multiclock Esterel. In Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\/PSTV). Edited by: Latella D, Bolognesi T, Latella D . Kluwer Pisa; 2000:301-316."},{"key":"22_CR47","first-page":"3","volume-title":"Formal Methods and Models for Codesign (MEMOCODE)","author":"N Halbwachs","year":"2005","unstructured":"Halbwachs N: A synchronous language at work: the story of Lustre. In Formal Methods and Models for Codesign (MEMOCODE). IEEE Computer Society Verona; 2005:3-11."},{"key":"22_CR48","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/3-540-18317-5_15","volume-title":"Functional, Programming Languages and Computer Architecture, Volume 274 of LNCS","author":"T Gautier","year":"1987","unstructured":"Gautier T, Le Guernic P, Besnard L: SIGNAL, a declarative language for synchronous programming of real-time systems. In Functional, Programming Languages and Computer Architecture, Volume 274 of LNCS. Edited by: Kahn G. Springer Portland; 1987:257-277."},{"issue":"9","key":"22_CR49","doi-asserted-by":"publisher","first-page":"1321","DOI":"10.1109\/5.97301","volume":"79","author":"P Le Guernic","year":"1991","unstructured":"Le Guernic P, Gauthier T, Le Borgne M, Le Maire C: Programming real-time applications with SIGNAL. Proc. IEEE 1991,79(9):1321-1336. 10.1109\/5.97301","journal-title":"Proc. IEEE"},{"issue":"3","key":"22_CR50","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1142\/S0218126603000763","volume":"12","author":"P Le Guernic","year":"2003","unstructured":"Le Guernic P, Talpin JP, Le Lann JC: Polychrony for system design. J. Circuits Syst. Comput. (JCSC) 2003,12(3):261-304. 10.1142\/S0218126603000763","journal-title":"J. Circuits Syst. Comput. (JCSC)"},{"key":"22_CR51","first-page":"67","volume-title":"Application of Concurrency to System Design (ACSD)","author":"D Potop-Butucaru","year":"2004","unstructured":"Potop-Butucaru D, Caillaud B, Benveniste A: Concurrency in synchronous systems. In Application of Concurrency to System Design (ACSD). IEEE Computer Society Hamilton; 2004:67-76."},{"key":"22_CR52","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/ACSD.2005.10","volume-title":"Application of Concurrency to System Design (ACSD)","author":"D Potop-Butucaru","year":"2005","unstructured":"Potop-Butucaru D, Caillaud B: Correct-by-construction asynchronous implementation of modular synchronous specifications. In Application of Concurrency to System Design (ACSD). IEEE Computer Society Saint-Malo; 2005:48-57."}],"container-title":["EURASIP Journal on Embedded Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/1687-3963-2013-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1186\/1687-3963-2013-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/1687-3963-2013-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,4,30]],"date-time":"2017-04-30T17:21:12Z","timestamp":1493572872000},"score":1,"resource":{"primary":{"URL":"https:\/\/jes-eurasipjournals.springeropen.com\/articles\/10.1186\/1687-3963-2013-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,10]]},"references-count":52,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["22"],"URL":"https:\/\/doi.org\/10.1186\/1687-3963-2013-3","relation":{},"ISSN":["1687-3963"],"issn-type":[{"value":"1687-3963","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,10]]},"article-number":"3"}}