{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T15:00:49Z","timestamp":1773327649920,"version":"3.50.1"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2013,3,1]],"date-time":"2013-03-01T00:00:00Z","timestamp":1362096000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Timed automata with deadlines (TAD) are a form of timed automata that admit a more natural representation of urgent actions, with the additional advantage of avoiding the most common form of timelocks. We offer a compositional translation of a practically useful subset of TAD to timed safety automata (the well-known variant of timed automata where time progress conditions are expressed by invariants). More precisely, we translate networks of TAD to the modeling language of\n            <jats:sc>Uppaal<\/jats:sc>\n            , a state-of-the-art verification tool for timed automata. We also describe an implementation of this translation, which allows\n            <jats:sc>Uppaal<\/jats:sc>\n            to aid the design and analysis of TAD models.\n          <\/jats:p>","DOI":"10.1007\/s00165-011-0185-4","type":"journal-article","created":{"date-parts":[[2011,6,28]],"date-time":"2011-06-28T06:15:48Z","timestamp":1309241748000},"page":"289-318","source":"Crossref","is-referenced-by-count":15,"title":["Model-checking timed automata with deadlines with Uppaal"],"prefix":"10.1145","volume":"25","author":[{"given":"Rodolfo","family":"G\u00f3mez","sequence":"first","affiliation":[{"name":"Scivisum Ltd, Suite D, The Clocktower, 25-39 St George\u2019s Street, CT1 2LE, Canterbury, Kent, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00334-1"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_3_2","unstructured":"Blair GS Blair L Bowman H et\u00a0al (1998) Formal specification of distributed multimedia systems. UCL Press"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.104"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Behrmann G David A Larsen K (2004) A tutorial on Uppaal. In: SFM-RT 2004. LNCS 3185 pp 200\u2013236. Springer New York","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050032"},{"key":"e_1_2_1_2_7_2","unstructured":"Bowman H Gomez R (2006) Concurrency theory calculi and automata for modelling untimed and timed concurrent systems. Springer Berlin"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bozga M Graf S Ober I Ober I Sifakis J (2004) The IF toolset. In: SFM-RT 2004. LNCS vol 3185. Springer Berlin pp 237\u2013267","DOI":"10.1007\/978-3-540-30080-9_8"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bohnenkamp HC Hermanns H Katoen J-P (2007) MOTOR: the MODEST tool environment. In: TACAS\u201907. LNCS vol 4424 pp 500\u2013504. Springer Berlin","DOI":"10.1007\/978-3-540-71209-1_38"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Bowman H (2001) Time and action lock freedom properties for timed automata. In: Proceedings of FORTE 2001. Kluwer Dordrecht pp 119\u2013134","DOI":"10.1007\/0-306-47003-9_8"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Bornot S Sifakis J (1998) On the composition of hybrid systems. In: Hybrid systems: computation and control. LNCS vol 1386. Springer Berlin pp 49\u201363","DOI":"10.1007\/3-540-64358-3_31"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Bornot S Sifakis J Tripakis S (1998) Modeling urgency in timed systems. In: Proceedings of COMPOS 1997. LNCS vol 1536. Springer Berlin pp 103\u2013129","DOI":"10.1007\/3-540-49213-5_5"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-003-0135-6"},{"key":"e_1_2_1_2_14_2","unstructured":"Gomez R (2008) Verification of timed automata with deadlines in Uppaal. TR 2-08-2008 Computing Laboratory University of Kent"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Gomez R (2009) A compositional translation from timed automata with deadlines to Uppaal timed automata. In: 7th international conference on formal modelling and analysis of timed systems (FORMATS\u201909). LNCS vol 5813 Budapest Hungary September 2009. Springer Berlin pp 179\u2013194","DOI":"10.1007\/978-3-642-04368-0_15"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Gebremichael B Vaandrager F Zhang M (2006) Analysis of the zeroconf protocol using Uppaal. In: EMSOFT \u201906. ACM Press pp 242\u2013251","DOI":"10.1145\/1176887.1176923"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Havelund K Skou A Larsen KG Lund K (1997) Formal modeling and analysis of an audio\/video protocol: an industrial case study using Uppaal. In: IEEE real-time systems symposium RTSS \u201997. IEEE Computer Society pp 2\u201313","DOI":"10.7146\/brics.v4i31.18957"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"issue":"3","key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/s100090100048","article-title":"Formal design and analysis of a gearbox controller","volume":"3","author":"Lindahl M","year":"2001","journal-title":"Softw Tools Technol Transf"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Moller F Tofts C (1990) A temporal calculus of communicating systems. In: Proceedings of CONCUR 1990. Springer New York pp 401\u2013415","DOI":"10.1007\/BFb0039073"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Sifakis J Yovine S (1996) Compositional specification of timed systems. In: Proceedings of STACS\u201996. LNCS vol 1046. Springer Berlin pp 347\u2013359","DOI":"10.1007\/3-540-60922-9_29"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008734703554"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0008-1"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050009"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0185-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0185-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0185-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:54:05Z","timestamp":1641484445000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0185-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["10.1007\/s00165-011-0185-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0185-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3]]}}}