{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T17:39:03Z","timestamp":1751391543777},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2019,6,18]],"date-time":"2019-06-18T00:00:00Z","timestamp":1560816000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,6,18]],"date-time":"2019-06-18T00:00:00Z","timestamp":1560816000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2019,8]]},"DOI":"10.1007\/s11704-017-6485-y","type":"journal-article","created":{"date-parts":[[2018,4,27]],"date-time":"2018-04-27T10:42:39Z","timestamp":1524825759000},"page":"715-734","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL"],"prefix":"10.1007","volume":"13","author":[{"given":"Zhibin","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Paul","family":"Bodeveix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mamoun","family":"Filali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,18]]},"reference":[{"key":"6485_CR1","first-page":"477","volume":"13","author":"D Harel","year":"1989","unstructured":"Harel D, Pnueli A. On the development of reactive systems. Logics and Models of Concurrent Systems, 1989, F(13): 477\u2013498","journal-title":"Logics and Models of Concurrent Systems"},{"key":"6485_CR2","first-page":"1","volume-title":"The Embedded Systems Handbook","author":"D Potop-Butucaru","year":"2005","unstructured":"Potop-Butucaru D, De Simone R, Talpin J P. The synchronous hypothesis and synchronous languages. The Embedded Systems Handbook, 2005, 1\u201321"},{"issue":"9","key":"6485_CR3","doi-asserted-by":"publisher","first-page":"1293","DOI":"10.1109\/5.97299","volume":"79","author":"F Boussinot","year":"1991","unstructured":"Boussinot F, De Simone R. The Esterel language. Proceedings of the IEEE, 1991, 79(9): 1293\u20131304","journal-title":"Proceedings of the IEEE"},{"issue":"9","key":"6485_CR4","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. Proceedings of the IEEE, 1991, 79(9): 1305\u20131320","journal-title":"Proceedings of the IEEE"},{"issue":"2","key":"6485_CR5","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","volume":"16","author":"A Benveniste","year":"1991","unstructured":"Benveniste A, Le Guernic P, Jacquemot C. Synchronous programming with events and relations: the SIGNAL language and its semantics. Science of Computer Programming, 1991, 16(2): 103\u2013149","journal-title":"Science of Computer Programming"},{"key":"6485_CR6","volume-title":"Kaiserslautern: University of Kaiserslautern","author":"K Schneider","year":"2010","unstructured":"Schneider K. The synchronous programming language QUARTZ. Internal Report. Kaiserslautern: University of Kaiserslautern, 2010"},{"issue":"5","key":"6485_CR7","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1109\/MDT.2007.151","volume":"24","author":"P Teehan","year":"2007","unstructured":"Teehan P, Greenstreet M, Lemieux G. A survey and taxonomy of GALS design styles. IEEE Design and Test of Computers, 2007, 24(5): 418\u2013428","journal-title":"IEEE Design and Test of Computers"},{"key":"6485_CR8","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-48320-9_13","volume-title":"Proceedings of International Conference on Concurrency Theory.","author":"A Benveniste","year":"1999","unstructured":"Benveniste A, Caillaud B, Le Guernic P. From synchrony to asynchrony. In: Proceedings of International Conference on Concurrency Theory. 1999, 162\u2013177"},{"key":"6485_CR9","volume-title":"Technical Report.","author":"P Feautrier","year":"2013","unstructured":"Feautrier P, Gamati\u00e9 A, Gonnord L. Enhancing the compilation of synchronous dataflow programs with a combined numerical-boolean abstraction. Technical Report. 2013"},{"key":"6485_CR10","volume-title":"Proceedings of Synchronous Languages, Applications, and Programming.","author":"A Gamati\u00e9","year":"2006","unstructured":"Gamati\u00e9 A, Gautier T, Le Guernic P. Towards static analysis of SIGNAL programs using interval techniques. In: Proceedings of Synchronous Languages, Applications, and Programming. 2006"},{"key":"6485_CR11","first-page":"182","volume-title":"Proceedings of the 15th Annual IEEE International Conference andWorkshop on Engineering of Computer Based Systems.","author":"A Gamati\u00e9","year":"2008","unstructured":"Gamati\u00e9 A, Gautier T, Besnard L. An interval-based solution for static analysis in the SIGNAL language. In: Proceedings of the 15th Annual IEEE International Conference andWorkshop on Engineering of Computer Based Systems. 2008, 182\u2013190"},{"issue":"8","key":"6485_CR12","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E W Dijkstra","year":"1975","unstructured":"Dijkstra E W. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 1975, 18(8): 453\u2013457","journal-title":"Communications of the ACM"},{"key":"6485_CR13","first-page":"1","volume-title":"Proceedings of Forum on Specification and Design Languages.","author":"J Brandt","year":"2011","unstructured":"Brandt J, Gemunde M, Shukla S K, Talpin J P. Integrating system descriptions by clocked guarded actions. In: Proceedings of Forum on Specification and Design Languages. 2011, 1\u20138"},{"key":"6485_CR14","volume-title":"Internal Report 382\/11, Kaiserslautern: University of Kaiserslautern","author":"J Brandt","year":"2011","unstructured":"Brandt J, Schneider K. Separate translation of synchronous programs to guarded actions. Internal Report 382\/11, Kaiserslautern: University of Kaiserslautern, 2011"},{"key":"6485_CR15","first-page":"47","volume-title":"Proceedings of the ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems.","author":"J Brandt","year":"2010","unstructured":"Brandt J, Schneider K, Shukla S K. Translating concurrent action oriented specifications to synchronous guarded actions. In: Proceedings of the ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems. 2010, 47\u201356"},{"issue":"8","key":"6485_CR16","doi-asserted-by":"publisher","first-page":"854","DOI":"10.1109\/TVLSI.2006.878473","volume":"14","author":"S A Edwards","year":"2006","unstructured":"Edwards S A, Tardieu O. SHIM: a deterministic model for heterogeneous embedded systems. IEEE Transactions on Very Large Scale Integration Systems, 2006, 14(8): 854\u2013867","journal-title":"IEEE Transactions on Very Large Scale Integration Systems"},{"key":"6485_CR17","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10617-012-9087-9","volume":"18","author":"J Brandt","year":"2014","unstructured":"Brandt J, Gemunde M, Schneider K, Shukla A K, Talpin J P. Representation of synchronous, asynchronous, and polychronous components by clocked guarded actions. Design Automation for Embedded Systems, 2014, 18: 63\u201397","journal-title":"Design Automation for Embedded Systems"},{"key":"6485_CR18","unstructured":"ESPRIT project: safety critical embedded systems SACRES. The declarative code DC+, version 1.4. Technical Report, 1997"},{"key":"6485_CR19","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/2609248.2609259","volume-title":"Proceedings of the 17th ACM International Workshop on Software and Compilers for Embedded Systems.","author":"Z B Yang","year":"2014","unstructured":"Yang Z B, Bodeveix J P, Filali M, Hu K, Ma D F. A verified transformation: from polychronous programs to a variant of clocked guarded actions. In: Proceedings of the 17th ACM International Workshop on Software and Compilers for Embedded Systems. 2014, 128\u2013137"},{"issue":"1","key":"6485_CR20","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s11704-015-4364-y","volume":"10","author":"Z B Yang","year":"2016","unstructured":"Yang Z B, Bodeveix J P, Filali M, Hu K, Zhao Y W, Ma D F. Towards a verified compiler prototype for the synchronous language SIGNAL. Frontiers of Computer Science, 2016, 10(1): 37\u201353","journal-title":"Frontiers of Computer Science"},{"key":"6485_CR21","volume-title":"RTCA Inc.","author":"RTCA\/DO-178B","year":"1992","unstructured":"RTCA\/DO-178B. Software considerations in airborne systems and equipment certification. RTCA Inc., 1992"},{"key":"6485_CR22","volume-title":"RTCA Inc.","author":"RTCA\/DO-178C","year":"2011","unstructured":"RTCA\/DO-178C. Software considerations in airborne systems and equipment certification. RTCA Inc., 2011"},{"key":"6485_CR23","volume-title":"Universit\u00e9 Paris-Sud, LRI","author":"M Pouzet","year":"2016","unstructured":"Pouzet M. Lucid Synchrone, version 3: tutorial and reference manual. Universit\u00e9 Paris-Sud, LRI, 2016"},{"key":"6485_CR24","volume-title":"Toulouse: Universit\u00e9 de Toulouse","author":"J Forget","year":"2009","unstructured":"Forget J. A synchronous language for critical embedded systems with multiple real-time constraints. Dissertation for the Doctoral Degree. Toulouse: Universit\u00e9 de Toulouse, 2009"},{"key":"6485_CR25","volume-title":"New York: Springer","author":"P Cast\u00e9ran","year":"2004","unstructured":"Cast\u00e9ran P, Bertot Y. Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. New York: Springer, 2004"},{"key":"6485_CR26","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1145\/1596550.1596582","volume-title":"Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming","author":"B Pagano","year":"2009","unstructured":"Pagano B, Andrieu O, Moniot T, Canou B, Chailloux E, Wang P, Manoury P, Cola\u00e7o J L. Using objective Caml to develop safety-critical embedded tools in a certification framework. In: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, 2009, 215\u2013220"},{"key":"6485_CR27","first-page":"21","volume-title":"Proceedings of the 14th European Symposium on Programming.","author":"P Cousot","year":"2005","unstructured":"Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X. The ASTR\u00c9E analyzer. In: Proceedings of the 14th European Symposium on Programming. 2005: 21\u201330"},{"key":"6485_CR28","volume-title":"SIGNAL V4 Reference Manual","author":"L Besnard","year":"2010","unstructured":"Besnard L, Gautier T, Le Guernic P. SIGNAL V4 Reference Manual, 2010"},{"key":"6485_CR29","volume-title":"Springer Science and Business Media","author":"A Gamati\u00e9","year":"2009","unstructured":"Gamati\u00e9 A. Designing Embedded Systems with the Signal Programming Language: Synchronous, Reactive Specification. Springer Science and Business Media, 2009"},{"key":"6485_CR30","first-page":"413","volume-title":"Advanced Topics in Data-Flow Computing","author":"P Le Guernic","year":"1991","unstructured":"Le Guernic P, Gautier T. Data-Flow to von Neumann: the SIGNAL approach. Advanced Topics in Data-Flow Computing, 1991, 413\u2013438"},{"issue":"03","key":"6485_CR31","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1142\/S0218126603000763","volume":"12","author":"P Le Guernic","year":"2003","unstructured":"Le Guernic P, Talpin J P, Le Lann J C. Polychrony for system design. Journal of Circuits, Systems, and Computers, 2003, 12(03): 261\u2013303","journal-title":"Journal of Circuits, Systems, and Computers"},{"key":"6485_CR32","first-page":"151","volume-title":"Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems.","author":"A Pnueli","year":"1998","unstructured":"Pnueli A, Siegel M, Singerman E. Translation validation. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 1998, 151\u2013166"},{"key":"6485_CR33","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-642-35722-0_24","volume-title":"Proceedings of International Symposium on Logical Foundations of Computer Science.","author":"J P Talpin","year":"2013","unstructured":"Talpin J P, Brandt J, Gemunde M, Schneider K, Shukla S K. Constructive polychronous systems. In: Proceedings of International Symposium on Logical Foundations of Computer Science. 2013, 335\u2013349"},{"issue":"7","key":"6485_CR34","doi-asserted-by":"publisher","first-page":"917","DOI":"10.1109\/TSE.2012.85","volume":"39","author":"J Brandt","year":"2013","unstructured":"Brandt J, Gemunde M, Schneider K, Shukla S K, Talpin J P. Embedding polychrony into synchrony. IEEE Transactions on Software Engineering, 2013, 39(7): 917\u2013929","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"5","key":"6485_CR35","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1007\/s11704-013-3908-2","volume":"7","author":"Z B Yang","year":"2013","unstructured":"Yang Z B, Bodeveix J P, Filali M. A comparative study of two formal semantics of the SIGNAL language. Frontiers of Computer Science, 2013, 7(5): 673\u2013693","journal-title":"Frontiers of Computer Science"},{"key":"6485_CR36","volume-title":"Dissertation for the Doctoral Degree.","author":"T Amagbegnon","year":"1994","unstructured":"Amagbegnon T, Besnard L, Le Guernic P. Arborescent canonical form of boolean expressions. Dissertation for the Doctoral Degree. 1994"},{"key":"6485_CR37","first-page":"109","volume-title":"Proceedings of the 9th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE).","author":"B A Jose","year":"2011","unstructured":"Jose B A, Gamati\u00e9 A, Ouy J, Shukla S K. SMT based false causal loop detection during code synthesis from polychronous specifications. In: Proceedings of the 9th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE). 2011, 109\u2013118"},{"key":"6485_CR38","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-35308-6_2","volume-title":"Proceedings of International Conference on Certified Programs and Proofs","author":"X Leroy","year":"2012","unstructured":"Leroy X. Mechanized semantics for compiler verification. In: Proceedings of International Conference on Certified Programs and Proofs. 2012, 4\u20136"},{"issue":"7","key":"6485_CR39","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107\u2013115","journal-title":"Communications of the ACM"},{"issue":"5","key":"6485_CR40","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"G C Necula","year":"2000","unstructured":"Necula G C. Translation validation for an optimizing compiler. ACM SIGPLAN Notices, 2000, 35(5): 83\u201394","journal-title":"ACM SIGPLAN Notices"},{"key":"6485_CR41","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.","author":"G C Necula","year":"1997","unstructured":"Necula G C. Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1997, 106\u2013119"},{"key":"6485_CR42","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11581741_10","volume-title":"Proceedings of European Conference on Model Driven Architecture-Foundations and Applications.","author":"K Chen","year":"2005","unstructured":"Chen K, Sztipanovits J, Abdelwalhed S, Jackson E. Semantic anchoring with model transformations. In: Proceedings of European Conference on Model Driven Architecture-Foundations and Applications. 2005, 115\u2013129"},{"key":"6485_CR43","first-page":"4","volume-title":"Electronic Communications of the EASST","author":"A Narayanan","year":"2006","unstructured":"Narayanan A, Karsai G. Using semantic anchoring to verify behavior preservation in graph transformations. Electronic Communications of the EASST, 2006, 4"},{"issue":"5","key":"6485_CR44","doi-asserted-by":"publisher","first-page":"598","DOI":"10.1007\/s11704-013-3905-5","volume":"7","author":"J P Talpin","year":"2013","unstructured":"Talpin J P, Gautier T, Le Guernic P, Besnard L. Formal verification of synchronous data-flow program transformations toward certified compilers. Frontiers of Computer Science, 2013, 7(5): 598\u2013616","journal-title":"Frontiers of Computer Science"},{"key":"6485_CR45","first-page":"113","volume-title":"Proceedings of International Conference on Integrated Formal Methods.","author":"J P Talpin","year":"2012","unstructured":"Talpin J P, Gautier T, Le Guernic P, Besnard L. Formal verification of compiler transformations on polychronous equations. In: Proceedings of International Conference on Integrated Formal Methods. 2012, 113\u2013127"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-017-6485-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-017-6485-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-017-6485-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T09:27:14Z","timestamp":1693646834000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-017-6485-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,18]]},"references-count":45,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["6485"],"URL":"https:\/\/doi.org\/10.1007\/s11704-017-6485-y","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,6,18]]},"assertion":[{"value":"30 September 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 June 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}