{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:52:15Z","timestamp":1750308735926,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"2s","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014,1]]},"abstract":"<jats:p>The synchronous model of computation requires that in every step, inputs are read and outputs are synchronously computed as the reaction of the program. In addition, all internal variables are updated in parallel even though not all of these values might be required for the current and the future reaction steps. To avoid unnecessary computations, we present a compile-time optimization procedure that computes for every variable a condition that determines whether its value is required for current or future computations. In this sense, our optimizations allow us to identify passive code that can be disabled to avoid unnecessary computations and therefore to reduce the reaction time of programs or their energy consumption.<\/jats:p>","DOI":"10.1145\/2544375.2544387","type":"journal-article","created":{"date-parts":[[2014,2,4]],"date-time":"2014-02-04T14:16:21Z","timestamp":1391523381000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Passive code in synchronous programs"],"prefix":"10.1145","volume":"13","author":[{"given":"Jens","family":"Brandt","sequence":"first","affiliation":[{"name":"University of Kaiserslautern, Kaiserslautern, Germany"}]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern, Kaiserslautern, Germany"}]},{"given":"Yu","family":"Bai","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern, Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2014,1,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/390013.808479"},{"volume-title":"Dependency analysis of synchronous programming languages. M. S. thesis. Department of Computer Science","author":"Bai Y.","key":"e_1_2_1_2_1","unstructured":"Y. Bai . 2010. Dependency analysis of synchronous programming languages. M. S. thesis. Department of Computer Science , University of Kaiserslautern , Germany. Y. Bai. 2010. Dependency analysis of synchronous programming languages. M. S. thesis. Department of Computer Science, University of Kaiserslautern, Germany."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2011.22"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_2_1_5_1","unstructured":"G. Berry. 1999. The constructive semantics of pure Esterel. http:\/\/www-sop.inria.fr\/esterel.org\/.  G. Berry. 1999. The constructive semantics of pure Esterel. http:\/\/www-sop.inria.fr\/esterel.org\/."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"R.\n      Bloem H. N.\n      Gabow and \n      F.\n      Somenzi\n  . \n  2000\n  . An algorithm for strongly connected component analysis in n log n symbolic steps. In Formal Methods in Computer-Aided Design (FMCAD). W. A. Hunt and S. D. Johnson Eds. Lecture Notes in Computer Science vol. \n  1954 Springer 37--54.   R. Bloem H. N. Gabow and F. Somenzi. 2000. An algorithm for strongly connected component analysis in n log n symbolic steps. In Formal Methods in Computer-Aided Design (FMCAD). W. A. Hunt and S. D. Johnson Eds. Lecture Notes in Computer Science vol. 1954 Springer 37--54.","DOI":"10.1007\/3-540-40922-X_4"},{"volume-title":"Proceedings of the 12th International Workshop on Software Compilers for Embedded Systems (SCOPES). H. Falk, Ed., ACM, 1--10","author":"Brandt J.","key":"e_1_2_1_8_1","unstructured":"J. Brandt and K. Schneider . 2009a. Separate compilation for synchronous programs . In Proceedings of the 12th International Workshop on Software Compilers for Embedded Systems (SCOPES). H. Falk, Ed., ACM, 1--10 . J. Brandt and K. Schneider. 2009a. Separate compilation for synchronous programs. In Proceedings of the 12th International Workshop on Software Compilers for Embedded Systems (SCOPES). H. Falk, Ed., ACM, 1--10."},{"volume-title":"Proceedings of the 7th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE). R. Bloem and P. Schaumont, Eds., IEEE Computer Society, 161--170","author":"Brandt J.","key":"e_1_2_1_9_1","unstructured":"J. Brandt and K. Schneider . 2009b. Static data-flow analysis of synchronous programs . In Proceedings of the 7th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE). R. Bloem and P. Schaumont, Eds., IEEE Computer Society, 161--170 . J. Brandt and K. Schneider. 2009b. Static data-flow analysis of synchronous programs. In Proceedings of the 7th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE). R. Bloem and P. Schaumont, Eds., IEEE Computer Society, 161--170."},{"key":"e_1_2_1_10_1","unstructured":"J. Brandt and K. Schneider. 2011. Separate translation of synchronous programs to guarded actions. Internal report 382\/11 Department of Computer Science University of Kaiserslautern Kaiserslautern Germany.  J. Brandt and K. Schneider. 2011. Separate translation of synchronous programs to guarded actions. Internal report 382\/11 Department of Computer Science University of Kaiserslautern Kaiserslautern Germany."},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"K. M. Chandy and J. Misra. 1989. Parallel Program Design. Addison-Wesley Austin Texas.   K. M. Chandy and J. Misra. 1989. Parallel Program Design. Addison-Wesley Austin Texas.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"R.\n      Cleaveland M.\n      Klein and \n      B.\n      Steffen\n  . \n  1993\n  . Faster model checking for the modal &mu;-calculus. In Computer Aided Verification (CAV) G. von Bochmann and D. Probst Eds. Lecture Notes in Computer Science vol. \n  663 Springer 410--422.   R. Cleaveland M. Klein and B. Steffen. 1993. Faster model checking for the modal &mu;-calculus. In Computer Aided Verification (CAV) G. von Bochmann and D. Probst Eds. Lecture Notes in Computer Science vol. 663 Springer 410--422.","DOI":"10.1007\/3-540-56496-9_32"},{"key":"e_1_2_1_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"TAXYS: A tool for the development and verification of real-time embedded systems. In Computer Aided Verification (CAV)","author":"Closse E.","year":"2001","unstructured":"E. Closse , M. Poize , J. Pulou , J. Sifakis , P. Venter , D. Weil , and S. Yovine . 2001 . TAXYS: A tool for the development and verification of real-time embedded systems. In Computer Aided Verification (CAV) , G. Berry, H. Comon, and A. Finkel, Eds., Lecture Notes in Computer Science , vol. 2102 . Springer , 391--395. E. Closse, M. Poize, J. Pulou, J. Sifakis, P. Venter, D. Weil, and S. Yovine. 2001. TAXYS: A tool for the development and verification of real-time embedded systems. In Computer Aided Verification (CAV), G. Berry, H. Comon, and A. Finkel, Eds., Lecture Notes in Computer Science, vol. 2102. Springer, 391--395."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80443-8"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90269-0"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90031-1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"volume-title":"Computer Aided Verification (CAV)","author":"Dill D. L.","key":"e_1_2_1_18_1","unstructured":"D. L. Dill . 1996. The Murphi verification system . In Computer Aided Verification (CAV) , R. Alur and T. Henzinger, Eds., Lecture Notes in Computer Science, vol. 1102 . Springer , 390--393. D. L. Dill. 1996. The Murphi verification system. In Computer Aided Verification (CAV), R. Alur and T. Henzinger, Eds., Lecture Notes in Computer Science, vol. 1102. Springer, 390--393."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.980257"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.027"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"E. A.\n      Emerson C. S.\n      Jutla and \n      A. P.\n      Sistla\n  . \n  1993\n  . On model-checking for fragments of &mu;-calculus. In Computer Aided Verification (CAV) C. Courcoubetis Ed. Lecture Notes in Computer Science vol. \n  697\n  . \n  Springer 385--396.   E. A. Emerson C. S. Jutla and A. P. Sistla. 1993. On model-checking for fragments of &mu;-calculus. In Computer Aided Verification (CAV) C. Courcoubetis Ed. Lecture Notes in Computer Science vol. 697. Springer 385--396.","DOI":"10.1007\/3-540-56922-7_32"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00034-7"},{"volume-title":"Synchronous Programming of Reactive Systems","author":"Halbwachs N.","key":"e_1_2_1_23_1","unstructured":"N. Halbwachs . 1993. Synchronous Programming of Reactive Systems . Kluwer . N. Halbwachs. 1993. Synchronous Programming of Reactive Systems. Kluwer."},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"N.\n      Halbwachs P.\n      Raymond and \n      C.\n      Ratel\n  . \n  1991\n  . Generating efficient code from data-flow programs. In Programming Language Implementation and Logic Programming (PLILP) J. Maluszy\u0144ski and M. Wirsing Eds. Lecture Notes in Computer Science vol. \n  528\n  . \n  Springer 207--218.  N. Halbwachs P. Raymond and C. Ratel. 1991. Generating efficient code from data-flow programs. In Programming Language Implementation and Logic Programming (PLILP) J. Maluszy\u0144ski and M. Wirsing Eds. Lecture Notes in Computer Science vol. 528. Springer 207--218.","DOI":"10.1007\/3-540-54444-5_100"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512946"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/321832.321835"},{"key":"e_1_2_1_27_1","volume-title":"XEEMU: An improved XScale power simulator. In Power and Timing Modelling, Optimization and Simulation (PATMOS)","author":"Herczeg Z.","year":"2007","unstructured":"Z. Herczeg , A. Kiss , D. Schmidt , N. Wehn , and T. Gyim\u00f3thy . 2007 . XEEMU: An improved XScale power simulator. In Power and Timing Modelling, Optimization and Simulation (PATMOS) , N. Azemard and L. Svensson, Eds., Lecture Notes in Computer Science, vol. 4644 . Springer , 300--309. Z. Herczeg, A. Kiss, D. Schmidt, N. Wehn, and T. Gyim\u00f3thy. 2007. XEEMU: An improved XScale power simulator. In Power and Timing Modelling, Optimization and Simulation (PATMOS), N. Azemard and L. Svensson, Eds., Lecture Notes in Computer Science, vol. 4644. Springer, 300--309."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90011-W"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629911.1630132"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837288"},{"key":"e_1_2_1_31_1","unstructured":"H. J\u00e4rvinen and R. Kurki-Suonio. 1990. The DisCo language and temporal logic of actions. Tech. rep. 11. Software Systems Laboratory Tampere University of Technology.  H. J\u00e4rvinen and R. Kurki-Suonio. 1990. The DisCo language and temporal logic of actions. Tech. rep. 11. Software Systems Laboratory Tampere University of Technology."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"volume-title":"Proceedings of the Design, Automation and Test in Europe (DATE). IEEE Computer Society, 10196--10203","author":"Logothetis G.","key":"e_1_2_1_33_1","unstructured":"G. Logothetis and K. Schneider . 2003. Exact high level WCET analysis of synchronous programs by symbolic state space exploration . In Proceedings of the Design, Automation and Test in Europe (DATE). IEEE Computer Society, 10196--10203 . G. Logothetis and K. Schneider. 2003. Exact high level WCET analysis of synchronous programs by symbolic state space exploration. In Proceedings of the Design, Automation and Test in Europe (DATE). IEEE Computer Society, 10196--10203."},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"L.\n      Mendondca de Moura\n     and \n      N.\n      Bj\u00f8rner\n  . \n  2008\n  . Z3: An efficient SMT solver. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). C. Ramakrishnan and J. Rehof Eds. Lecture Notes in Computer Science vol. \n  4963\n  . \n  Springer 337--340.   L. Mendondca de Moura and N. Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). C. Ramakrishnan and J. Rehof Eds. Lecture Notes in Computer Science vol. 4963. Springer 337--340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/823453.823835"},{"key":"e_1_2_1_36_1","unstructured":"D. Potop-Butucaru S. A. Edwards and G. Berry. 2007. Compiling Esterel. Springer.   D. Potop-Butucaru S. A. Edwards and G. Berry. 2007. Compiling Esterel. Springer."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/359842.359849"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268950"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the IFIP International Workshop on Distributed and Parallel Embedded Systems (DIPES). F. Rammig, Ed. Kluwer, 205--214","author":"Schneider K.","year":"2000","unstructured":"K. Schneider . 2000 . A verified hardware synthesis for Esterel . In Proceedings of the IFIP International Workshop on Distributed and Parallel Embedded Systems (DIPES). F. Rammig, Ed. Kluwer, 205--214 . K. Schneider. 2000. A verified hardware synthesis for Esterel. In Proceedings of the IFIP International Workshop on Distributed and Parallel Embedded Systems (DIPES). F. Rammig, Ed. Kluwer, 205--214."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/784820.784830"},{"key":"e_1_2_1_42_1","first-page":"39","article-title":"Improving automata generation for linear temporal logic by considering the automata hierarchy. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), R. Nieuwenhuis and A. Voronkov, Eds","volume":"2250","author":"Schneider K.","year":"2001","unstructured":"K. Schneider . 2001 b. Improving automata generation for linear temporal logic by considering the automata hierarchy. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), R. Nieuwenhuis and A. Voronkov, Eds ., Lecture Notes in Artificial Intelligence , vol. 2250 , Spring er, 39 -- 54 . K. Schneider. 2001b. Improving automata generation for linear temporal logic by considering the automata hierarchy. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), R. Nieuwenhuis and A. Voronkov, Eds., Lecture Notes in Artificial Intelligence, vol. 2250, Springer, 39--54.","journal-title":"Lecture Notes in Artificial Intelligence"},{"key":"e_1_2_1_43_1","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics (TPHOL)","author":"Schneider K.","unstructured":"K. Schneider . 2002. Proving the equivalence of microstep and macrostep semantics . In Theorem Proving in Higher Order Logics (TPHOL) , V. Carre\u00f1o, C. Mu\u00f1oz, and S. Tahar, Eds., Lecture Notes in Computer Science , vol. 2410 . Springer , 314--331. K. Schneider. 2002. Proving the equivalence of microstep and macrostep semantics. In Theorem Proving in Higher Order Logics (TPHOL), V. Carre\u00f1o, C. Mu\u00f1oz, and S. Tahar, Eds., Lecture Notes in Computer Science, vol. 2410. Springer, 314--331."},{"volume-title":"Verification of Reactive Systems - Formal Methods and Algorithms. Texts in Theoretical Computer Science","author":"Schneider K.","key":"e_1_2_1_44_1","unstructured":"K. Schneider . 2003. Verification of Reactive Systems - Formal Methods and Algorithms. Texts in Theoretical Computer Science , Springer . K. Schneider. 2003. Verification of Reactive Systems - Formal Methods and Algorithms. Texts in Theoretical Computer Science, Springer."},{"volume-title":"Proceedings of the 8th International Conference on Application of Concurrency to System Design (ACSD). IEEE Computer Society, 78--87","author":"Schneider K.","key":"e_1_2_1_46_1","unstructured":"K. Schneider and J. Brandt . 2008. Performing causality analysis by bounded model checking . In Proceedings of the 8th International Conference on Application of Concurrency to System Design (ACSD). IEEE Computer Society, 78--87 . K. Schneider and J. Brandt. 2008. Performing causality analysis by bounded model checking. In Proceedings of the 8th International Conference on Application of Concurrency to System Design (ACSD). IEEE Computer Society, 78--87."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1023833.1023859"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.028"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996602"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0898-1221(81)90008-0"},{"volume-title":"Proceedings of the Conference on Theoretical Aspects of Computer Software (TACS)","author":"Steffen B.","key":"e_1_2_1_51_1","unstructured":"B. Steffen . 1991. Data flow analysis as model checking . In Proceedings of the Conference on Theoretical Aspects of Computer Software (TACS) . T. Ito and A.R. Meyer, Eds., Lecture Notes in Computer Science, vol. 526 . Springer , 346--364. B. Steffen. 1991. Data flow analysis as model checking. In Proceedings of the Conference on Theoretical Aspects of Computer Software (TACS). T. Ito and A.R. Meyer, Eds., Lecture Notes in Computer Science, vol. 526. Springer, 346--364."},{"key":"e_1_2_1_52_1","unstructured":"SYNC98 SYNCHRON. 1998. The common format of synchronous languages - the declarative code DC. Tech. rep. C2A SYNCHRON project.  SYNC98 SYNCHRON. 1998. The common format of synchronous languages - the declarative code DC. Tech. rep. C2A SYNCHRON project."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760275"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.875347"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/997163.997188"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2544375.2544387","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2544375.2544387","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:04Z","timestamp":1750278124000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2544375.2544387"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1]]},"references-count":55,"journal-issue":{"issue":"2s","published-print":{"date-parts":[[2014,1]]}},"alternative-id":["10.1145\/2544375.2544387"],"URL":"https:\/\/doi.org\/10.1145\/2544375.2544387","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2014,1]]},"assertion":[{"value":"2012-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-01-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}