{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:46:35Z","timestamp":1761324395538,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2021,9,22]],"date-time":"2021-09-22T00:00:00Z","timestamp":1632268800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Foundation of Science of China","award":["61972076"],"award-info":[{"award-number":["61972076"]}]},{"name":"Hong Kong RGC","award":["GRF 15204917"],"award-info":[{"award-number":["GRF 15204917"]}]},{"name":"National Foundation of Science of China","award":["U1808206"],"award-info":[{"award-number":["U1808206"]}]},{"name":"European Research Concil CUSTOMER","award":["834166"],"award-info":[{"award-number":["834166"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2021,10,31]]},"abstract":"<jats:p>Research on modeling and analysis of real-time computing systems has been done in two areas, model checking and real-time scheduling theory. In model checking, an expressive modeling formalism such as timed automata (TA) is used to model complex systems, but the analysis is typically very expensive due to state-space explosion. In real-time scheduling theory, the analysis techniques are highly efficient, but the models are often restrictive. In this paper, we aim to exploit the possibility of applying efficient analysis techniques rooted in real-time scheduling theory to analysis of real-time task systems modeled by timed automata with tasks (TAT). More specifically, we develop efficient techniques to analyze the feasibility of TAT-based task models (i.e., whether all tasks can meet their deadlines on single-processor) using demand bound functions (DBF), a widely used workload abstraction in real-time scheduling theory. Our proposed analysis method has a pseudo-polynomial time complexity if the number of clocks used to model each task is bounded by a constant, which is much lower than the exponential complexity of the traditional model-checking based analysis approach (also assuming the number of clocks is bounded by a constant). We apply dynamic programming techniques to implement the DBF-based analysis framework, and propose state space pruning techniques to accelerate the analysis process. Experimental results show that our DBF-based method can analyze a TAT system with 50 tasks within a few minutes, which significantly outperforms the state-of-the-art TAT-based schedulability analysis tool TIMES.<\/jats:p>","DOI":"10.1145\/3477020","type":"journal-article","created":{"date-parts":[[2021,9,22]],"date-time":"2021-09-22T20:48:40Z","timestamp":1632343720000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Schedulability Analysis for Timed Automata With Tasks"],"prefix":"10.1145","volume":"20","author":[{"given":"Jinghao","family":"Sun","sequence":"first","affiliation":[{"name":"Dalian University of Technology, Dalian City, Liaoning Province, China China"}]},{"given":"Nan","family":"Guan","sequence":"additional","affiliation":[{"name":"City University of Hong Kong, Hong Kong, China"}]},{"given":"Rongxiao","family":"Shi","sequence":"additional","affiliation":[{"name":"Northeastern University, Shenyang City, Liaoning Province, China"}]},{"given":"Guozhen","family":"Tan","sequence":"additional","affiliation":[{"name":"Dalian University of Technology, Dalian City, Liaoning Province, China China"}]},{"given":"Wang","family":"Yi","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2021,9,22]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Formal Methods for Timing Verification (FMTV) challenge 2016. http:\/\/waters2016.inria.fr\/challenge\/.  Formal Methods for Timing Verification (FMTV) challenge 2016. http:\/\/waters2016.inria.fr\/challenge\/."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.018"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765894"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/838237.838662"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/647770.734246"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694613"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2010.19"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008030427220"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021711220939"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Sanjoy K. Baruah et al.1990. Preemptively scheduling hard-real-time sporadic tasks on one processor. In RTSS.  Sanjoy K. Baruah et al.1990. Preemptively scheduling hard-real-time sporadic tasks on one processor. In RTSS.","DOI":"10.1109\/REAL.1990.128746"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/647767.733781"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2005.21"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/648063.747438"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2003.07.005"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647767.733772"},{"key":"e_1_2_1_19_1","volume-title":"Clarke et al.1999. State space reduction using partial order techniques. IJSTTT","author":"Edmund","year":"1999","unstructured":"Edmund M. Clarke et al.1999. State space reduction using partial order techniques. IJSTTT ( 1999 ). Edmund M. Clarke et al.1999. State space reduction using partial order techniques. IJSTTT (1999)."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/789083.1022725"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765893"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.01.009"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.2004.17"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSSC.1968.300136"},{"key":"e_1_2_1_25_1","unstructured":"Pavel Krc\u00e1l et al.2007. A tool for compositional analysis of timed systems by abstraction. In NWPT07.  Pavel Krc\u00e1l et al.2007. A tool for compositional analysis of timed systems by abstraction. In NWPT07."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-010-9055-1"},{"key":"e_1_2_1_27_1","unstructured":"Kim Guldstrand Larsen etal1997. Efficient verification of real-time systems: Compact data structure and state-space reduction. In RTSS.  Kim Guldstrand Larsen et al.1997. Efficient verification of real-time systems: Compact data structure and state-space reduction. In RTSS."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321743"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016720.1016753"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/530225"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACIRS.2018.8467245"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.637146"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2007.16"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2008.47"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2009.24"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90067-6"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-015-9234-z"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2011.15"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2018.00472"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477020","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3477020","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:46Z","timestamp":1750188646000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3477020"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,22]]},"references-count":41,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2021,10,31]]}},"alternative-id":["10.1145\/3477020"],"URL":"https:\/\/doi.org\/10.1145\/3477020","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2021,9,22]]},"assertion":[{"value":"2021-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-09-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}