{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T10:27:59Z","timestamp":1750933679766},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"5-6","license":[{"start":{"date-parts":[[2015,11,1]],"date-time":"2015-11-01T00:00:00Z","timestamp":1446336000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The paper presents a new efficient algorithm for computing worst case execution time (WCET) of systems modelled as timed automata (TA). The algorithm uses a set of abstraction techniques that improve significantly the efficiency of WCET analysis of TA models with cyclic behaviour. We show that the proposed abstractions are exact with respect to the WCET problem in the sense that the WCET computed in the abstract model is equal to the one computed in the concrete model. We also compare our algorithm with the one implemented in the model checker UPPAAL which shows that when infinite cycles exist (i.e. cycles that can be run infinitely often), UPPAAL\u2019s algorithm may not terminate, and when largely repetitive finite cycles exist (i.e. cycles that can be run a large number of times but finite), UPPAAL\u2019s algorithm suffers from the state space explosion, thus leading to a low efficiency or resource exhaustion.<\/jats:p>","DOI":"10.1007\/s00165-015-0340-4","type":"journal-article","created":{"date-parts":[[2015,7,30]],"date-time":"2015-07-30T06:16:32Z","timestamp":1438236992000},"page":"917-949","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Accelerating worst case execution time analysis of timed automata models with cyclic behaviour"],"prefix":"10.1145","volume":"27","author":[{"given":"Omar","family":"Al-Bataineh","sequence":"first","affiliation":[{"name":"School of Computer Science and Software Engineering, University of Western Australia, Perth, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Reynolds","sequence":"additional","affiliation":[{"name":"School of Computer Science and Software Engineering, University of Western Australia, Perth, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"French","sequence":"additional","affiliation":[{"name":"School of Computer Science and Software Engineering, University of Western Australia, Perth, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Al-Bataineh O (2015) Verifying worst-case execution time of timed automata models with cyclic behaviour. Ph.D. thesis University of Western Australia Perth Australia","DOI":"10.1007\/s00165-015-0340-4"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Al-Bataineh O Reynolds M French T (2014) Finding best and worst case execution times of systems using difference-bound matrices. In: FORMATS\u201914 Lecture notes in computer science. Springer Berlin","DOI":"10.1007\/978-3-319-10512-3_4"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Alur R Dill D (1994) A theory of timed automata. In: TCS pp 183\u2013235","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_4_2","unstructured":"Alur R (1998) Timed automata. In: NATO ASI summer school on verification of digital and hybrid systems"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bardin S Finkel A Leroux J Schnoebelen P (2005) Flat acceleration in symbolic model checking. In: Automated technology for verification and analysis third international symposium ATVA 2005 Taipei Taiwan October 4\u20137 2005 Proceedings pp 474\u2013488","DOI":"10.1007\/11562948_35"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bardin S Leroux J Point G (2006) FAST extended release. In: Computer aided verification 18th international conference CAV 2006 Seattle WA USA August 17\u201320 2006 Proceedings pp 63\u201366","DOI":"10.1007\/11817963_9"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Behrmann G Fehnker A Hune T Larsen K Pettersson P Romijn J (2001) Efficient guiding towards cost-optimality in uppaal. In: Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems TACAS 2001. Springer Berlin pp 174\u2013188","DOI":"10.1007\/3-540-45319-9_13"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Behrmann G Bouyer P Fleury E Larsen KG (2003) Static guard analysis in timed automata verification. In: Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems TACAS\u201903. Springer Berlin pp 254\u2013270","DOI":"10.1007\/3-540-36577-X_18"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Behrmann G David A Larsen KG (2004) A tutorial on Uppaal. In: Formal methods for the design of real-time systems (SFM-RT 2004). Springer Berlin pp 200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Behrmann G Larsen KG Rasmussen JI (2005) Beyond liveness: efficient parameter synthesis for time bounded liveness. In: FORMATS pp 81\u201394","DOI":"10.1007\/11603009_7"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Behrmann G Bouyer P Larsen KG Radek P (2006) Lower and upper bounds in zone-based abstractions of timed automata. Int J Softw Tools Technol Transf 204\u2013215","DOI":"10.1007\/s10009-005-0190-0"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Bengtsson J Yi W (2004) Timed automata: semantics algorithms and tools. In: Lecture notes on concurrency and petri nets. Springer Berlin","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Boigelot B Wolper P (1994) Symbolic verification with periodic sets. In: Computer aided verification 6th international conference CAV \u201994 Stanford California USA June 21\u201323 1994 Proceedings pp 55\u201367","DOI":"10.1007\/3-540-58179-0_43"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Boigelot B Godefroid P Willems B Wolper P (1997) The power of QDDs (extended abstract). In: Static analysis 4th international symposium SAS \u201997 Paris France September 8\u201310 1997 Proceedings pp 172\u2013186","DOI":"10.1007\/BFb0032741"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008719024240"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000026093.21513.31"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0010-7"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Bozga M Iosif R Konecn\u00fd F (2010) Fast acceleration of ultimately periodic relations. In: Computer aided verification 22nd international conference CAV 2010 Edinburgh UK July 15\u201319 2010. Proceedings pp 227\u2013242","DOI":"10.1007\/978-3-642-14295-6_23"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Clarke EM Grumberg O Peled D (2001) Model checking. MIT Press Cambridge","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"e_1_2_1_2_21_2","unstructured":"Dalsgaard AE Olesen MC Toft M Hansen RR Larsen KG (2010) METAMOC: modular execution time analysis using model checking. In: 10th international workshop on worst-case execution time analysis (WCET 2010) pp 113\u2013123"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Dalsgaard AE Hansen RR Jrgensen KY Larsen KG Olesen MC Olsen P Srba J (2011) opaal: a lattice model checker. In: NASA formal methods\u201911 pp 487\u2013493","DOI":"10.1007\/978-3-642-20398-5_37"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Daws C Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In: Proceedings of the 4th international conference on tools and algorithms for construction and analysis of systems TACAS \u201998. Springer London pp 313\u2013329","DOI":"10.1007\/BFb0054180"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Daws C Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In: Proceedings of the 4th international conference on tools and algorithms for construction and analysis of systems TACAS \u201998. Springer London pp 313\u2013329.","DOI":"10.1007\/BFb0054180"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Dill D (1990) Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of the international workshop on automatic verification methods for finite state systems Springer New York pp 197\u2013212","DOI":"10.1007\/3-540-52148-8_17"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Fietzke A Kruglov E Weidenbach C (2012) Automatic generation of invariants for circular derivations in SUP(LA). In: Logic for programming artificial intelligence and reasoning\u201418th international conference LPAR-18 M\u00e9rida Venezuela March 11\u201315 2012. Proceedings pp 197\u2013211","DOI":"10.1007\/978-3-642-28717-6_17"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Floyd RW (1962) Algorithm 97: shortest path. Commun ACM","DOI":"10.1145\/367766.368168"},{"key":"e_1_2_1_2_28_2","unstructured":"G\u00f3mez R (2006) Verification of real-time systems: improving tool support. Ph.D. thesis Computing Laboratory University of Kent"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Hendriks M Larsen KG (2002) Exact acceleration of real-time model checking. Electr Notes Theor Comput Sci 65(6):120\u2013139","DOI":"10.1016\/S1571-0661(04)80473-0"},{"key":"e_1_2_1_2_30_2","unstructured":"Huber B Schoeberl M (2009) Comparison of implicit path enumeration and model checking based WCET analysis. In: Holsti N (ed) 9th international workshop on worst-case execution time analysis (WCET\u201909) OpenAccess series in informatics (OASIcs) vol 10. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik Wadern pp 1\u201312"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Metzner A (2004) Why model checking can improve WCET analysis. In: Proceeding of the international conference on computer-aided verification (CAV) pp 334\u2013347","DOI":"10.1007\/978-3-540-27813-9_26"},{"key":"e_1_2_1_2_32_2","unstructured":"Pettersson P (1999) Modelling and verification of real-time systems using timed automata: theory and practice. Ph.D. thesis Uppsala University"},{"key":"e_1_2_1_2_33_2","unstructured":"Rokicki TG (1993) Representing and modeling digital circuits. Ph.D. thesis Stanford University"},{"key":"e_1_2_1_2_34_2","unstructured":"Salah RB (2007) On timing analysis of large systems. Ph.D. thesis Institut National Polytechnique De Grenoble"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Wilhelm R 2004 Why AI +\u00a0 ILP is good for WCET but MC is not nor ILP alone. In: Steffen B Levi G (eds) VMCAI pp 309\u2013322","DOI":"10.1007\/978-3-540-24622-0_25"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-015-0340-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-015-0340-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-015-0340-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:09:54Z","timestamp":1641485394000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-015-0340-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11]]},"references-count":35,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["10.1007\/s00165-015-0340-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-015-0340-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,11]]}}}