{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T17:16:23Z","timestamp":1791479783170,"version":"4.3.4"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4-5","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2008,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Model checking of real-time systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to realistic applications. Our algorithm significantly extends the subset of DC that can be checked automatically. The central part of the algorithm is the automatic decomposition of DC specifications into sub-properties that can be verified independently. The decomposition is based on a novel distributive law for DC. We implemented the algorithm in a tool chain for the automated verification of systems comprising data, communication, and real-time aspects. We applied the tool chain to verify safety properties in an industrial case study from the European Train Control System (ETCS).<\/jats:p>","DOI":"10.1007\/s00165-008-0082-7","type":"journal-article","created":{"date-parts":[[2008,5,5]],"date-time":"2008-05-05T08:59:30Z","timestamp":1209977970000},"page":"481-505","source":"Crossref","is-referenced-by-count":28,"title":["Model checking Duration Calculus: a practical approach"],"prefix":"10.1145","volume":"20","author":[{"given":"Roland","family":"Meyer","sequence":"first","affiliation":[{"name":"Department f\u00fcr Informatik, Carl von Ossietzky Universit\u00e4t Oldenburg, 26111, Oldenburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Johannes","family":"Faber","sequence":"additional","affiliation":[{"name":"Department f\u00fcr Informatik, Carl von Ossietzky Universit\u00e4t Oldenburg, 26111, Oldenburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jochen","family":"Hoenicke","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Albert-Ludwigs Universit\u00e4t Freiburg, 79110, Freiburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, 66123, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"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","first-page":"196","volume-title":"CAV, LNCS, vol 939","author":"Bouajjani A","year":"1995"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Ball T Majumdar R Millstein T Rajamani S (2001) Automatic predicate abstraction of C programs. In: PLDI volume 36 of ACM SIGPLAN Notices. ACM Press New York pp 203\u2013213","DOI":"10.1145\/381694.378846"},{"key":"e_1_2_1_2_5_2","first-page":"54","volume-title":"Integrated Formal Methods, LNCS, vol 4591","author":"Br\u00fcckner I","year":"2007"},{"key":"e_1_2_1_2_6_2","first-page":"154","volume-title":"CAV, LNCS, vol 1855","author":"Clarke EM","year":"2000"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cook B Podelski A Rybalchenko A (2005) Abstraction refinement for termination. In: SAS LNCS vol 3672. Springer Heidelberg pp 87\u2013101","DOI":"10.1007\/11547662_8"},{"key":"e_1_2_1_2_8_2","first-page":"433","volume-title":"FTRTFT, LNCS, vol 2469","author":"Dierks H","year":"2002"},{"key":"e_1_2_1_2_9_2","unstructured":"ECSAG. ERTMS\/ETCS Functional requirements specification (1999)"},{"key":"e_1_2_1_2_10_2","unstructured":"ERTMS User Group UNISIG. ERTMS\/ETCS System requirements specification (2002)"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Fr\u00e4nzle M Hansen MR (2007) Deciding an interval logic with accumulated durations. In: TACAS LNCS vol 4424. Springer Heidelberg pp 201\u2013215","DOI":"10.1007\/978-3-540-71209-1_17"},{"key":"e_1_2_1_2_12_2","first-page":"233","volume-title":"Integrated Formal Methods. LNCS, vol 4591","author":"Faber J","year":"2007"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-004-0032-y"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Graf S Saidi H (1997) Construction of abstract state graphs with PVS. In: Grumberg O (ed.) CAV vol 1254. Springer Heidelberg pages 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_1_2_15_2","unstructured":"Hansen M (2006) DC with nominals. Personal communication March (2006)"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"POPL","author":"Henzinger TA","year":"2004"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Hermanns H Jansen DN Usenko YS (2005) From StoCharts to MoDeST: a comparative reliability analysis of train radio communications. In: WOSP. ACM Press New York pp 13\u201323","DOI":"10.1145\/1071021.1071023"},{"key":"e_1_2_1_2_18_2","first-page":"465","volume-title":"FM, LNCS, vol 3582","author":"Hoenicke J","year":"2005"},{"key":"e_1_2_1_2_19_2","unstructured":"Hoenicke J Meyer R Faber J (2006) PEA toolkit home page. http:\/\/csd.informatik.uni-oldenburg.de\/projects\/epea.html"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Hoenicke J Olderog ER (2002) CSP-OZ-DC: A combination of specification techniques for processes data and time. Nordic J Comput 9","DOI":"10.1007\/3-540-47884-1_14"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_22_2","unstructured":"Hoenicke J (2006) Combination of Processes Data and Time. Ph.D. thesis University of Oldenburg"},{"key":"e_1_2_1_2_23_2","first-page":"444","volume-title":"FSTTCS, LNCS, vol 3821","author":"Krishna SN","year":"2005"},{"key":"e_1_2_1_2_24_2","first-page":"1","volume-title":"CAV, LNCS, vol 2725","author":"McMillan KL","year":"2003"},{"key":"e_1_2_1_2_25_2","first-page":"332","volume-title":"ICTAC, LNCS, vol 4281","author":"Meyer R","year":"2006"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Pandya PK (2002) Interval duration logic: Expressiveness and decidability. ENTCS 65(6)","DOI":"10.1016\/S1571-0661(04)80480-8"},{"key":"e_1_2_1_2_27_2","first-page":"216","volume-title":"TABLEAUX, LNCS, vol 4548","author":"Platzer A","year":"2007"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Podelski A Rybalchenko A (2005) Transition predicate abstraction and fair termination. In: POPL. ACM Press New York pp 132\u2013144","DOI":"10.1145\/1047659.1040317"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Podelski A Rybalchenko A (2007) ARMC: the logical choice for software model checking with abstraction refinement. In: PADL LNCS vol 4281. Springer Heidelberg pp 245\u2013259","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"e_1_2_1_2_30_2","unstructured":"Ravn AP (1994) Design of Embedded Real-Time Computing Systems. Ph.D. thesis Technical University of Denmark"},{"key":"e_1_2_1_2_31_2","volume-title":"Theory and Practice of Concurrency","author":"Roscoe AW","year":"1998"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Rybalchenko A Sofronie-Stokkermans V (2007) Constraint solving for interpolation. In: VMCAI LNCS vol 4349. Springer Heidelberg pp. 346\u2013362","DOI":"10.1007\/978-3-540-69738-1_25"},{"key":"e_1_2_1_2_33_2","unstructured":"Rybalchenko A (2007) ARMC. http:\/\/www.mpi-sws.mpg.de\/~rybal\/armc"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"e_1_2_1_2_35_2","unstructured":"Uppaal home page. University of Aalborg and University of Uppsala. http:\/\/www.uppaal.com 1995\u20132005"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"e_1_2_1_2_37_2","unstructured":"Vardi MY Wolper P (1986) An automata-theoretic approach to automatic program verification. In: LICS. IEEE Computer Society pp 332\u2013344"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.5555\/975040"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2003.12.039"},{"key":"e_1_2_1_2_40_2","first-page":"58","volume-title":"STACS, LNCS, vol 665","author":"Zhou C","year":"1993"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-008-0082-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:47:30Z","timestamp":1641484050000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-008-0082-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7]]},"references-count":40,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["10.1007\/s00165-008-0082-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-008-0082-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,7]]}}}