{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:21:05Z","timestamp":1760080865837,"version":"3.41.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2023,9,9]],"date-time":"2023-09-09T00:00:00Z","timestamp":1694217600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2023,10,31]]},"abstract":"<jats:p>\n            Scade is a domain-specific synchronous functional language used to implement safety-critical real-time software for more than twenty years. Two main approaches have been considered for its semantics: (i) an\n            <jats:italic>indirect collapsing semantics<\/jats:italic>\n            based on a source-to-source translation of high-level constructs into a data-flow core language whose semantics is precisely specified and is the entry for code generation; a\n            <jats:italic>relational synchronous semantics<\/jats:italic>\n            , akin to Esterel, that applies\n            <jats:italic>directly<\/jats:italic>\n            to the source. It defines what is a valid synchronous reaction but hides, on purpose, if a semantics exists, is unique and can be computed; hence, it is not executable.\n          <\/jats:p>\n          <jats:p>\n            This paper presents, for the first time, an\n            <jats:italic>executable<\/jats:italic>\n            , state-based semantics for a language that has the key constructs of Scade all together, in particular the arbitrary combination of data-flow equations and hierarchical state machines. It can apply\n            <jats:italic>directly<\/jats:italic>\n            to the source language before static checks and compilation steps. It is\n            <jats:italic>constructive<\/jats:italic>\n            in the sense that the language in which the semantics is defined is a statically typed functional language with call-by-value and strong normalization, e.g., it is expressible in a proof-assistant where all functions terminate. It leads to a reference, purely functional, interpreter. This semantics is modular and can account for possible errors, allowing to establish what property is ensured by each static verification performed by the compiler. It also clarifies how causality is treated in Scade compared with Esterel.\n          <\/jats:p>\n          <jats:p>This semantics can serve as an oracle for compiler testing and validation; to prototype novel language constructs before they are implemented, to execute possibly unfinished models or that are correct but rejected by the compiler; to prove the correctness of compilation steps.<\/jats:p>\n          <jats:p>The semantics given in the paper is implemented as an interpreter in a purely functional style, in OCaml.<\/jats:p>","DOI":"10.1145\/3609131","type":"journal-article","created":{"date-parts":[[2023,9,9]],"date-time":"2023-09-09T13:33:18Z","timestamp":1694266398000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A Constructive State-based Semantics and Interpreter for a Synchronous Data-flow Language with State Machines"],"prefix":"10.1145","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3848-1826","authenticated-orcid":false,"given":"Jean-Louis","family":"Cola\u00e7o","sequence":"first","affiliation":[{"name":"Ansys, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9562-0576","authenticated-orcid":false,"given":"Michael","family":"Mendler","sequence":"additional","affiliation":[{"name":"The University of Bamberg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-8812-1381","authenticated-orcid":false,"given":"Baptiste","family":"Pauget","sequence":"additional","affiliation":[{"name":"Ansys, France and Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2651-7708","authenticated-orcid":false,"given":"Marc","family":"Pouzet","sequence":"additional","affiliation":[{"name":"ENS, France and PSL University, France and Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,9,9]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"86","volume-title":"ESOP","author":"Aguado Joaqu\u00edn","year":"2018","unstructured":"Joaqu\u00edn Aguado, Michael Mendler, Marc Pouzet, Partha S. Roop, and Reinhard von Hanxleden. 2018. Deterministic concurrency: A clock-synchronised shared memory approach. In ESOP. Thessaloniki, Greece, 86\u2013113."},{"issue":"4","key":"e_1_3_2_3_2","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1007\/s00236-015-0238-x","article-title":"Denotational fixed-point semantics for constructive scheduling of synchronous concurrency","volume":"52","author":"Aguado J.","year":"2015","unstructured":"J. Aguado, M. Mendler, R. von Hanxleden, and I. Fuhrmann. 2015. Denotational fixed-point semantics for constructive scheduling of synchronous concurrency. Acta Informatica 52, 4 (2015), 393\u2013442.","journal-title":"Acta Informatica"},{"key":"e_1_3_2_4_2","volume-title":"CESA","author":"Andr\u00e9 Ch.","year":"1996","unstructured":"Ch. Andr\u00e9. 1996. Representation and analysis of reactive behaviors: A synchronous approach. In CESA. IEEE-SMC, Lille."},{"key":"e_1_3_2_5_2","volume-title":"HSCC","author":"Benveniste A.","year":"2014","unstructured":"A. Benveniste, T. Bourke, B. Caillaud, B. Pagano, and M. Pouzet. 2014. A type-based analysis of causality loops in hybrid systems modelers. In HSCC. ACM, Berlin, Germany."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_3_2_7_2","volume-title":"Actors Without Directors: A Kahnian View of Heterogeneous Systems","author":"Benveniste A.","year":"2008","unstructured":"A. Benveniste, P. Caspi, R. Lublinerman, and S. Tripakis. 2008. Actors Without Directors: A Kahnian View of Heterogeneous Systems. Technical Report. Verimag, Centre \u00c9quation, 38610 Gi\u00e8res."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90001-E"},{"key":"e_1_3_2_9_2","article-title":"Real time programming: Special purpose or general purpose languages","author":"Berry G.","year":"1989","unstructured":"G. Berry. 1989. Real time programming: Special purpose or general purpose languages. Information Processing (1989).","journal-title":"Information Processing"},{"key":"e_1_3_2_10_2","article-title":"The semantics of pure esterel","volume":"118","author":"Berry G.","year":"1993","unstructured":"G. Berry. 1993. The semantics of pure esterel. Series F: Computer and System Sciences 118 (011993).","journal-title":"Series F: Computer and System Sciences"},{"key":"e_1_3_2_11_2","unstructured":"G. Berry. 2002. The Constructive Semantics of Pure Esterel Draft Version 3. (2002)."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_3_2_13_2","article-title":"Towards coq-verified esterel semantics and compiling","volume":"1909","author":"Berry G.","year":"2019","unstructured":"G. Berry and L. Rieg. 2019. Towards coq-verified esterel semantics and compiling. CoRR abs\/1909.12582 (2019).","journal-title":"CoRR"},{"key":"e_1_3_2_14_2","volume-title":"ACM LCTES","author":"Biernacki D.","year":"2008","unstructured":"D. Biernacki, J. L. Colaco, G. Hamon, and Marc Pouzet. 2008. Clock-directed modular code generation of synchronous data-flow languages. In ACM LCTES. Tucson, Arizona."},{"key":"e_1_3_2_15_2","volume-title":"LPAR","author":"Boulm\u00e9 S.","year":"2001","unstructured":"S. Boulm\u00e9 and G. Hamon. 2001. Certifying synchrony for free. In LPAR, Vol. 2250. La Havana, Cuba."},{"key":"e_1_3_2_16_2","volume-title":"PLDI","author":"Bourke T.","year":"2017","unstructured":"T. Bourke, L. Brun, P.-\u00c9. Dagand, X. Leroy, M. Pouzet, and L. Rieg. 2017. A formally verified compiler for Lustre. In PLDI."},{"key":"e_1_3_2_17_2","volume-title":"POPL","author":"Bourke T.","year":"2020","unstructured":"T. Bourke, L. Brun, and M. Pouzet. 2020. Mechanized semantics and verified compilation for a dataflow synchronous language with reset. In POPL. ACM."},{"key":"e_1_3_2_18_2","volume-title":"EMSOFT","author":"Bourke T.","year":"2023","unstructured":"T. Bourke, B. Pesin, and M. Pouzet. 2023. Verified compilation of synchronous dataflow with state machines. In EMSOFT."},{"key":"e_1_3_2_19_2","volume-title":"HSCC","author":"Bourke T.","year":"2013","unstructured":"T. Bourke and M. Pouzet. 2013. Z\u00e9lus, a synchronous language with ODEs. In HSCC. ACM, Philadelphia, USA."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90326-B"},{"key":"e_1_3_2_21_2","volume-title":"POPL","author":"Caspi P.","year":"1987","unstructured":"P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice. 1987. Lustre: A declarative language for programming synchronous systems. In POPL. ACM."},{"key":"e_1_3_2_22_2","volume-title":"ACM ICFP","author":"Caspi P.","year":"1996","unstructured":"P. Caspi and M. Pouzet. 1996. Synchronous kahn networks. In ACM ICFP. Philadelphia, Pensylvania."},{"key":"e_1_3_2_23_2","volume-title":"CMCS\u201998","author":"Caspi P.","year":"1998","unstructured":"P. Caspi and M. Pouzet. 1998. A co-iterative characterization of synchronous stream functions. In CMCS\u201998."},{"key":"e_1_3_2_24_2","volume-title":"ACM EMSOFT","author":"Cola\u00e7o J. L.","year":"2006","unstructured":"J. L. Cola\u00e7o, G. Hamon, and M. Pouzet. 2006. Mixing signals and modes in synchronous data-flow systems. In ACM EMSOFT. Seoul, South Korea."},{"key":"e_1_3_2_25_2","volume-title":"ACM EMSOFT","author":"Cola\u00e7o J. L.","year":"2005","unstructured":"J. L. Cola\u00e7o, B. Pagano, and M. Pouzet. 2005. A conservative extension of synchronous data-flow with state machines. In ACM EMSOFT. Jersey city, New Jersey, USA."},{"key":"e_1_3_2_26_2","volume-title":"ACM EMSOFT","author":"Cola\u00e7o J. L.","year":"2003","unstructured":"J. L. Cola\u00e7o and M. Pouzet. 2003. Clocks as first class abstract types. In ACM EMSOFT. Philadelphia, USA."},{"key":"e_1_3_2_27_2","volume-title":"Symposium on Theoretical Aspect of Software Engineering (TASE\u201917)","author":"Colaco J. L.","year":"2017","unstructured":"J. L. Colaco, B. Pagano, and M. Pouzet. 2017. Scade 6: A formal language for embedded critical software development. In Symposium on Theoretical Aspect of Software Engineering (TASE\u201917). Sophia Antipolis, France."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00096-5"},{"key":"e_1_3_2_29_2","unstructured":"G. Gonthier. 1988. S\u00e9mantiques et mod\u00e8les d\u2019ex\u00e9cution des langages r\u00e9actifs synchrones . Ph. D. Dissertation. Universit\u00e9 d\u2019Orsay."},{"key":"e_1_3_2_30_2","unstructured":"N. Halbwachs. 1984. Mod\u00e9lisation et analyse du comportement des syst\u00e8mes informatiques temporis\u00e9s . Ph. D. Dissertation. Institut National Polytechnique de Grenoble - INPG; Universit\u00e9 Joseph - Fourier - Grenoble I."},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_32_2","volume-title":"Third International Symposium on Programming Language Implementation and Logic Programming","author":"Halbwachs N.","year":"1991","unstructured":"N. Halbwachs, P. Raymond, and C. Ratel. 1991. Generating efficient code from data-flow programs. In Third International Symposium on Programming Language Implementation and Logic Programming. Passau (Germany)."},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","article-title":"StateCharts: A visual approach to complex systems","volume":"8","author":"Harel D.","year":"1987","unstructured":"D. Harel. 1987. StateCharts: A visual approach to complex systems. Science of Computer Programming 8-3 (1987), 231\u2013275.","journal-title":"Science of Computer Programming"},{"key":"e_1_3_2_34_2","first-page":"159","volume-title":"Arrows, Robots, and Functional Reactive Programming","author":"Hudak P.","year":"2003","unstructured":"P. Hudak, A. Courtney, H. Nilsson, and J. Peterson. 2003. Arrows, Robots, and Functional Reactive Programming. Springer, Berlin, 159\u2013187."},{"key":"e_1_3_2_35_2","first-page":"222","article-title":"A tutorial on (co)algebras and (co)induction","volume":"62","author":"Jacobs B.","year":"1997","unstructured":"B. Jacobs and J. Rutten. 1997. A tutorial on (co)algebras and (co)induction. EATCS Bulletin 62 (1997), 222\u2013259.","journal-title":"EATCS Bulletin"},{"key":"e_1_3_2_36_2","volume-title":"IFIP 74 Congress","author":"Kahn G.","year":"1974","unstructured":"G. Kahn. 1974. The semantics of a simple language for parallel programming. In IFIP 74 Congress. North Holland, Amsterdam."},{"issue":"12","key":"e_1_3_2_37_2","article-title":"A framework for comparing models of computation","volume":"17","author":"Lee E. A.","year":"1998","unstructured":"E. A. Lee and A. Sangiovanni-Vincentelli. 1998. A framework for comparing models of computation. IEEE Transactions on CAD 17, 12 (December1998).","journal-title":"IEEE Transactions on CAD"},{"key":"e_1_3_2_38_2","unstructured":"Xavier Leroy. 2021. The Compcert Verified Compiler. http:\/\/compcert.inria.fr\/doc\/index.html"},{"issue":"7","key":"e_1_3_2_39_2","doi-asserted-by":"crossref","DOI":"10.1109\/43.293952","article-title":"Analysis of cyclic combinational circuits","volume":"13","author":"Malik S.","year":"1994","unstructured":"S. Malik. 1994. Analysis of cyclic combinational circuits. IEEE Trans. on CAD of Integrated Circuits and Systems 13, 7 (1994).","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"e_1_3_2_40_2","volume-title":"IEEE Workshop on Visual Languages","author":"Maraninchi F.","year":"1991","unstructured":"F. Maraninchi. 1991. The Argos Language: Graphical representation of automata and description of reactive systems. In IEEE Workshop on Visual Languages. Kobe, Japan."},{"key":"e_1_3_2_41_2","volume-title":"AADEBUG\u20192000 \u2013 Fourth International Workshop on Automated Debugging","author":"Maraninchi F.","year":"2000","unstructured":"F. Maraninchi and F. Gaucher. 2000. Step-wise + algorithmic debugging for reactive programs: LuDiC, a debugger for Lustre. In AADEBUG\u20192000 \u2013 Fourth International Workshop on Automated Debugging. Munich."},{"issue":"46","key":"e_1_3_2_42_2","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/S0167-6423(02)00093-X","article-title":"Mode-automata: A new domain-specific construct for the development of safe critical systems","author":"Maraninchi F.","year":"2003","unstructured":"F. Maraninchi and Y. R\u00e9mond. 2003. Mode-automata: A new domain-specific construct for the development of safe critical systems. Science of Computer Programming46 (2003), 219\u2013254.","journal-title":"Science of Computer Programming"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1955.tb03788.x"},{"key":"e_1_3_2_44_2","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1145\/507635.507664","volume-title":"ICFP","author":"Paterson R.","year":"2001","unstructured":"R. Paterson. 2001. A new notation for arrows. In ICFP (Firenze, Italy). ACM Press, 229\u2013240."},{"key":"e_1_3_2_45_2","volume-title":"TYPES","author":"Paulin-Mohring C.","year":"1995","unstructured":"C. Paulin-Mohring. 1995. Circuits as streams in coq: Verification of a sequential multiplier. In TYPES. Springer."},{"key":"e_1_3_2_46_2","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1017\/CBO9780511770524.018","volume-title":"From Semantics to Computer Science","author":"Paulin-Mohring Ch.","year":"2009","unstructured":"Ch. Paulin-Mohring. 2009. A constructive denotational semantics for Kahn networks in Coq. In From Semantics to Computer Science, Y. Bertot, G. Huet, J. J. L\u00e9vy, and G. Plotkin (Eds.). Cambridge University Press, 383\u2013413."},{"key":"e_1_3_2_47_2","volume-title":"Lucid Synchrone, version 3. Tutorial and reference manual","author":"Pouzet M.","year":"2006","unstructured":"M. Pouzet. 2006. Lucid Synchrone, version 3. Tutorial and reference manual. Universit\u00e9 Paris-Sud, LRI."},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.5555\/307999"},{"key":"e_1_3_2_49_2","volume-title":"Handbook of Hardware\/Software Codesign","author":"Schneider Klaus","year":"2016","unstructured":"Klaus Schneider and Jens Brandt. 2016. Handbook of Hardware\/Software Codesign. S. Ha and J. Teich (Eds); Springer Science+Business Media Dordrecht, Chapter Quartz: A Synchronous Language for Model-Based Design of Reactive Embedded Systems."},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2005.24"},{"key":"e_1_3_2_51_2","volume-title":"SOS Workshop","author":"Tardieu O.","year":"2004","unstructured":"O. Tardieu. 2004. A deterministic logical semantics for esterel. In SOS Workshop. London, United Kingdom."},{"key":"e_1_3_2_52_2","volume-title":"PLDI\u201914","author":"Hanxleden R. von","year":"2014","unstructured":"R. von Hanxleden, B. Duderstadt, C. Motika, S. Smyth, M. Mendler, J. Aguado, S. Mercer, and O. O\u2019Brien. 2014. SCCharts: Sequentially constructive statecharts for safety-critical applications. In PLDI\u201914."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609131","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3609131","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:48:58Z","timestamp":1750182538000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609131"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,9]]},"references-count":51,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2023,10,31]]}},"alternative-id":["10.1145\/3609131"],"URL":"https:\/\/doi.org\/10.1145\/3609131","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2023,9,9]]},"assertion":[{"value":"2023-03-23","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-06-30","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}