{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:41:57Z","timestamp":1761324117060,"version":"3.41.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T00:00:00Z","timestamp":1506470400000},"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":[[2017,10,31]]},"abstract":"<jats:p>Synchronous languages are ideal for designing safety-critical systems. Static Worst-Case Reaction Time (WCRT) analysis is an essential component in the design flow that ensures the real-time requirements are met. There are a few approaches for WCRT analysis, and the most versatile of all is explicit path enumeration. However, as synchronous programs are highly concurrent, techniques based on this approach, such as model checking, suffer from state explosion as the number of threads increases. One observation on this problem is that these existing techniques analyse the program by enumerating a functionally equivalent automaton while WCRT is a non-functional property. This mismatch potentially causes algorithm-induced state explosion. In this paper, we propose a WCRT analysis technique based on the notion of timing equivalence, expressed using WCRT algebra. WCRT algebra can effectively capture the timing behaviour of a synchronous program by converting its intermediate representation Timed Concurrent Control Flow Graph (TCCFG) into a Tick Cost Automaton (TCA), a minimal automaton that is timing equivalent to the original program. Then the WCRT is computed over the TCA. We have implemented our approach and benchmarked it against state-of-the-art WCRT analysis techniques. The results show that the WCRT algebra is 3.5 times faster on average than the fastest published technique.<\/jats:p>","DOI":"10.1145\/3126520","type":"journal-article","created":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T12:33:53Z","timestamp":1506515633000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Timing Analysis of Synchronous Programs using WCRT Algebra"],"prefix":"10.1145","volume":"16","author":[{"given":"Jiajie","family":"Wang","sequence":"first","affiliation":[{"name":"University of Auckland, Auckland, New Zealand"}]},{"given":"Michael","family":"Mendler","sequence":"additional","affiliation":[{"name":"University of Bamberg"}]},{"given":"Partha","family":"Roop","sequence":"additional","affiliation":[{"name":"University of Auckland, Auckland, New Zealand"}]},{"given":"Bruno","family":"Bodin","sequence":"additional","affiliation":[{"name":"University of Edinburgh"}]}],"member":"320","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"volume-title":"Gurobi optimiser. (Nov","year":"2016","unstructured":"2016. Gurobi optimiser. (Nov . 2016 ). http:\/\/www.gurobi.com. 2016. Gurobi optimiser. (Nov. 2016). http:\/\/www.gurobi.com.","key":"e_1_2_1_1_1"},{"volume-title":"UPPAAL model checker. (Nov","year":"2016","unstructured":"2016. UPPAAL model checker. (Nov . 2016 ). http:\/\/www.uppaal.org. 2016. UPPAAL model checker. (Nov. 2016). http:\/\/www.uppaal.org.","key":"e_1_2_1_2_1"},{"doi-asserted-by":"crossref","unstructured":"J. Aguado M. Mendler J. J. Wang B. Bodin and P. Roop. 2017. Compositional timing-aware semantics for synchronous programming. In Forum on Specification and Design Languages (FDL\u20192017). Verona Italy.  J. Aguado M. Mendler J. J. Wang B. Bodin and P. Roop. 2017. Compositional timing-aware semantics for synchronous programming. In Forum on Specification and Design Languages (FDL\u20192017). Verona Italy.","key":"e_1_2_1_3_1","DOI":"10.1109\/FDL.2017.8303895"},{"key":"e_1_2_1_4_1","volume-title":"Automation Test in Europe Conference Exhibition (DATE). 1--6.","author":"Andalam Sidharta","year":"2011","unstructured":"Sidharta Andalam , Partha S. Roop , and Alain Girault . 2011 . Pruning infeasible paths for tight WCRT analysis of synchronous programs. In Design , Automation Test in Europe Conference Exhibition (DATE). 1--6. Sidharta Andalam, Partha S. Roop, and Alain Girault. 2011. Pruning infeasible paths for tight WCRT analysis of synchronous programs. In Design, Automation Test in Europe Conference Exhibition (DATE). 1--6."},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1109\/TC.2013.28"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1155\/2008\/594129"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1109\/DATE.2005.326"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1145\/1629911.1630132"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1007\/s11241-012-9155-z"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1145\/2024724.2024837"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1145\/216636.216666"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1007\/978-3-319-44878-7_12"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1007\/s11241-015-9219-y"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1145\/1629395.1629424"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/2594291.2594310"},{"doi-asserted-by":"crossref","unstructured":"Jia Jie Wang Partha S. Roop and Sidharta Andalam. 2013. ILPc: A novel approach for scalable timing analysis of synchronous programs. In Compilers Architecture and Synthesis for Embedded Systems (CASES). 1--10.   Jia Jie Wang Partha S. Roop and Sidharta Andalam. 2013. ILPc: A novel approach for scalable timing analysis of synchronous programs. In Compilers Architecture and Synthesis for Embedded Systems (CASES). 1--10.","key":"e_1_2_1_16_1","DOI":"10.1109\/CASES.2013.6662526"},{"doi-asserted-by":"crossref","unstructured":"Li Hsien Yoong Partha S. Roop and Zoran Salcic. 2013. Implementing constrained cyber-physical systems with IEC 61499. In ACM Transactions on Embedded Computing Systems (TECS). Number 1. ACM.  Li Hsien Yoong Partha S. Roop and Zoran Salcic. 2013. Implementing constrained cyber-physical systems with IEC 61499. In ACM Transactions on Embedded Computing Systems (TECS). Number 1. ACM.","key":"e_1_2_1_17_1","DOI":"10.1145\/2362336.2362345"},{"key":"e_1_2_1_18_1","volume-title":"Shaw","author":"Yoong Li Hsien","year":"2010","unstructured":"Li Hsien Yoong and Gareth D . Shaw . 2010 . Auckland Function Block Benchmark.University of Auckland . (2010). pretzel.ece.auckland.ac.nz\/files\/iec61499-benchmarks.zip. Li Hsien Yoong and Gareth D. Shaw. 2010. Auckland Function Block Benchmark.University of Auckland. (2010). pretzel.ece.auckland.ac.nz\/files\/iec61499-benchmarks.zip."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3126520","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3126520","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:01Z","timestamp":1750273501000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3126520"}},"subtitle":["Scalability through Abstraction"],"short-title":[],"issued":{"date-parts":[[2017,9,27]]},"references-count":18,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2017,10,31]]}},"alternative-id":["10.1145\/3126520"],"URL":"https:\/\/doi.org\/10.1145\/3126520","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2017,9,27]]},"assertion":[{"value":"2017-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}