{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T20:23:35Z","timestamp":1791231815579,"version":"4.1.0"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,10,5]],"date-time":"2022-10-05T00:00:00Z","timestamp":1664928000000},"content-version":"vor","delay-in-days":308,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1350574"],"award-info":[{"award-number":["CCF-1350574"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100010583","name":"Universit\u00e4t Konstanz","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100010583","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present algorithms and techniques for the repair of timed system models, given as networks of timed automata (NTA). The repair is based on an analysis of timed diagnostic traces (TDTs) that are computed by real-time model checking tools, such as UPPAAL, when they detect the violation of a timed safety property. We present an encoding of TDTs in linear real arithmetic and use the MaxSMT capabilities of the SMT solver Z3 to suggest a minimal number of possible syntactic repairs of the analyzed model. The suggested repairs include modified values for clock bounds in location invariants and transition guards, adding or removing clock resets, etc. We then present an admissibility criterion, called functional equivalence, which ensures that the proposed repair preserves the functional behavior of the considered NTA. We discuss a proof-of-concept tool called <jats:sc>TarTar<\/jats:sc> that we have developed, implementing the repair and admissibility analysis, and give insights into its design and architecture. We evaluate the proposed repair technique on faulty mutations generated from a diverse suite of case studies taken from the literature. We show that <jats:sc>TarTar<\/jats:sc> can admissibly repair for 69\u2013<jats:inline-formula><jats:alternatives><jats:tex-math>$$88\\%$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>88<\/mml:mn>\n                    <mml:mo>%<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> of the seeded errors in the considered system models.<\/jats:p>","DOI":"10.1007\/s10703-022-00397-5","type":"journal-article","created":{"date-parts":[[2022,10,5]],"date-time":"2022-10-05T18:02:47Z","timestamp":1664992967000},"page":"136-169","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Automated repair for timed systems"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8959-5332","authenticated-orcid":false,"given":"Martin","family":"K\u00f6lbl","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4259-624X","authenticated-orcid":false,"given":"Stefan","family":"Leue","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4051-5968","authenticated-orcid":false,"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,10,5]]},"reference":[{"key":"397_CR1","doi-asserted-by":"crossref","unstructured":"Andr\u00e9 \u00c9, Arcaini P, Gargantini A, Radavelli M (2019) Repairing timed automata clock guards through abstraction and testing. In: Beyer D, Keller C (eds) Tests and Proofs - 13th international conference, TAP@FM 2019, Porto, Portugal, October 9-11, 2019, Proceedings, volume 11823 of Lecture notes in computer science, pp 129\u2013146. Springer","DOI":"10.1007\/978-3-030-31157-5_9"},{"key":"397_CR2","unstructured":"Alur R, Bod\u00edk R, Dallal E, Fisman D, Garg P, Juniwal G, Kress-Gazit H, Madhusudan P, Martin Milo MK, Mukund R, Shambwaditya S, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2015) Syntax-guided synthesis. In: Dependable software systems engineering, volume\u00a040 of NATO Science for peace and security series, D: information and communication security, pp 1\u201325. IOS Press"},{"issue":"1","key":"397_CR3","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur R, Courcoubetis C, Dill DL (1993) Model-checking in dense real-time. Inf Comput 104(1):2\u201334","journal-title":"Inf Comput"},{"issue":"2","key":"397_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"issue":"3","key":"397_CR5","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern B, Schneider FB (1987) Recognizing safety and liveness. Distrib Comput 2(3):117\u2013126","journal-title":"Distrib Comput"},{"key":"397_CR6","doi-asserted-by":"publisher","first-page":"1001","DOI":"10.1007\/978-3-319-10575-8_29","volume-title":"Handbook of model checking","author":"P Bouyer","year":"2018","unstructured":"Bouyer P, Fahrenberg U, Larsen KG, Markey N, Ouaknine J, Worrell J (2018) Model checking real-time systems. Handbook of model checking. Springer, Berlin, pp 1001\u20131046"},{"key":"397_CR7","unstructured":"Barrett C, Fontaine P, Tinelli C (2017) SMT-lib, http:\/\/smtlib.cs.uiowa.edu\/language.shtml"},{"key":"397_CR8","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"397_CR9","doi-asserted-by":"crossref","unstructured":"Ben-Abdallah H, Leue S (1997) Timing constraints in message sequence chart specifications. In: FORTE, volume 107 of IFIP conference proceedings, pp 91\u2013106. Chapman and Hall","DOI":"10.1007\/978-0-387-35271-8_6"},{"key":"397_CR10","doi-asserted-by":"crossref","unstructured":"Bengtsson J, Larsen KG, Larsson F, Pettersson P, Yi W (1995) Uppaal - a tool suite for automatic verification of real-time systems. In: Hybrid systems, volume 1066 of Lecture notes in computer science, pp 232\u2013243. Springer, Berlin","DOI":"10.1007\/BFb0020949"},{"key":"397_CR11","doi-asserted-by":"crossref","unstructured":"Bend\u00edk J, Sencan A, Gol EA, Cern\u00e1 I (2021) Timed automata relaxation for reachability. In: Groote JF, Larsen KG (eds) Tools and algorithms for the construction and analysis of systems - 27th international conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27\u2013April 1, 2021, Proceedings, Part I, volume 12651 of Lecture notes in computer science, pp 291\u2013310. Springer","DOI":"10.1007\/978-3-030-72016-2_16"},{"key":"397_CR12","doi-asserted-by":"crossref","unstructured":"Bengtsson J, Yi W (2003) Timed automata: semantics, algorithms and tools. In: Lectures on concurrency and petri nets, volume 3098 of Lecture notes in computer science, pp 87\u2013124. Springer","DOI":"10.1007\/978-3-540-27755-2_3"},{"issue":"6","key":"397_CR13","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/0020-0190(93)90069-L","volume":"46","author":"EM Clarke","year":"1993","unstructured":"Clarke EM, Draghicescu IA, Kurshan RP (1993) A unified approach for showing language inclusion and equivalence between various types of omega-automata. Inf Process Lett 46(6):301\u2013308","journal-title":"Inf Process Lett"},{"key":"397_CR14","doi-asserted-by":"crossref","unstructured":"Czerbo DB (1992) Handbook of theoretical computer science: van leeuwen J (ed), vol. A: algorithms and complexity, vol. B: formal methods and semantics (Elsevier, Amsterdam, 1990), p 2296, hardcover, dfl. 555.00. Artif Intell Medicine 4(4):309","DOI":"10.1016\/0933-3657(92)90044-P"},{"issue":"1\/2","key":"397_CR15","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport JH, Heintz J (1988) Real quantifier elimination is doubly exponential. J Symb Comput 5(1\/2):29\u201335","journal-title":"J Symb Comput"},{"key":"397_CR16","doi-asserted-by":"crossref","unstructured":"Dalsgaard AE, Hansen RR, J\u00f8rgensen KY, Larsen KG, Olesen MC, Olsen P, Srba J (2011) opaal: A lattice model checker. In: NASA formal methods, volume 6617 of Lecture notes in computer science, pp 487\u2013493. Springer","DOI":"10.1007\/978-3-642-20398-5_37"},{"key":"397_CR17","doi-asserted-by":"crossref","unstructured":"Dierks H, Kupferschmid S, Larsen KG (2007) Automatic abstraction refinement for timed automata. In FORMATS, volume 4763 of Lecture notes in computer science, pp 114\u2013129. Springer","DOI":"10.1007\/978-3-540-75454-1_10"},{"key":"397_CR18","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS, volume 4963 of Lecture Notes in Computer Science, pp 337\u2013340. Springer","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"397_CR19","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/s00236-021-00403-z","volume":"59","author":"M Ergurtuna","year":"2022","unstructured":"Ergurtuna M, Yalcinkaya B, Gol EA (2022) An automated system repair framework with signal temporal logic. Acta Inf 59(2):183\u2013209","journal-title":"Acta Inf"},{"key":"397_CR20","unstructured":"Field A (2013) Discovering statistics using IBM SPSS statistics: and sex and drugs and rock \u2019n\u2019 roll, 4th Edition. Sage"},{"key":"397_CR21","unstructured":"Garey MR, Johnson DS (1979) Computers and intractability: a guide to the theory of NP-Completeness. W. H. Freeman"},{"key":"397_CR22","doi-asserted-by":"crossref","unstructured":"Ghosh S, Sadigh D, Nuzzo P, Raman V, Donz\u00e9 A, Sangiovanni-Vincentelli AL, Sastry SS, Seshia SA (2016) Diagnosis and repair for synthesis from signal temporal logic specifications. In: Abate A, Fainekos G (eds) Proceedings of the 19th international conference on hybrid systems: computation and control, HSCC 2016, Vienna, Austria, April 12\u201314, 2016, pp 31\u201340. ACM","DOI":"10.1145\/2883817.2883847"},{"issue":"2","key":"397_CR23","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"Henzinger TA, Nicollin X, Sifakis J, Yovine S (1994) Symbolic model checking for real-time systems. Inf Comput 111(2):193\u2013244","journal-title":"Inf Comput"},{"key":"397_CR24","volume-title":"Introduction to automata theory, languages and computation","author":"JE Hopcroft","year":"2000","unstructured":"Hopcroft JE, Ullman JD (2000) Introduction to automata theory, languages and computation, 2nd edn. Addison-Wesley, Boston","edition":"2"},{"key":"397_CR25","doi-asserted-by":"crossref","unstructured":"Isberner M, Howar F, Steffen B (2015) The open-source learnlib - A framework for active automata learning. In: CAV (1), volume 9206 of Lecture notes in computer science, pp 487\u2013495. Springer","DOI":"10.1007\/978-3-319-21690-4_32"},{"issue":"5","key":"397_CR26","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1109\/TSE.2010.62","volume":"37","author":"Y Jia","year":"2011","unstructured":"Jia Y, Harman M (2011) An analysis and survey of the development of mutation testing. IEEE Trans Softw Eng 37(5):649\u2013678","journal-title":"IEEE Trans Softw Eng"},{"key":"397_CR27","doi-asserted-by":"crossref","unstructured":"Jensen HE, Larsen KG, Skou A (1996) Modelling and analysis of a collision avoidance protocol using spin and uppaal. In: The Spin verification system, volume\u00a032 of DIMACS series in discrete mathematics and theoretical computer science, pp 33\u201350. DIMACS\/AMS","DOI":"10.1090\/dimacs\/032\/04"},{"key":"397_CR28","doi-asserted-by":"crossref","unstructured":"Jose M, Majumdar R (2011) Bug-assist: assisting fault localization in ANSI-C programs. In: CAV, volume 6806 of Lecture notes in computer science, pp 504\u2013509. Springer,","DOI":"10.1007\/978-3-642-22110-1_40"},{"key":"397_CR29","doi-asserted-by":"crossref","unstructured":"Jiang Z, Pajic M, Moarref S, Alur R, Mangharam R (2012) Modeling and verification of a dual chamber implantable pacemaker. In: TACAS, volume 7214 of Lecture notes in computer science, pp 188\u2013203. Springer","DOI":"10.1007\/978-3-642-28756-5_14"},{"key":"397_CR30","doi-asserted-by":"crossref","unstructured":"Karmarkar N (1984) A new polynomial-time algorithm for linear programming. In: Proceedings of the sixteenth annual ACM symposium on Theory of computing, pp 302-311","DOI":"10.1145\/800057.808695"},{"key":"397_CR31","doi-asserted-by":"crossref","unstructured":"K\u00f6lbl M, Leue S, Wies T (2019) Clock bound repair for timed systems. In: CAV (1), volume 11561 of Lecture notes in computer science, pp 79\u201396. Springer","DOI":"10.1007\/978-3-030-25540-4_5"},{"key":"397_CR32","doi-asserted-by":"crossref","unstructured":"K\u00f6lbl M, Leue S, Wies T (2020) Tartar: a timed automata repair tool. CoRR, arXiv:2002.02760. Also available from URL https:\/\/www.sen.uni-konstanz.de\/publications","DOI":"10.1007\/978-3-030-53288-8_25"},{"key":"397_CR33","doi-asserted-by":"crossref","unstructured":"Kroening D, Strichman O (2016) Decision procedures - an algorithmic point of view, Second Edition. Texts in theoretical computer science. An EATCS Series. Springer","DOI":"10.1007\/978-3-662-50497-0"},{"key":"397_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24488-9","volume-title":"Combinatorial optimization: theory and algorithms. Algorithms and combinatorics","author":"B Korte","year":"2012","unstructured":"Korte B, Vygen J (2012) Combinatorial optimization: theory and algorithms. Algorithms and combinatorics. Springer, Berlin Heidelberg"},{"key":"397_CR35","doi-asserted-by":"crossref","unstructured":"Le X-BD, Chu D-H, Lo D, Le GC, Visser W (2017) S3: syntax- and semantic-guided repair synthesis via programming by examples. In: Proceedings of the 2017 11th joint meeting on foundations of software engineering, ESEC\/FSE 2017, pp 593\u2013604. ACM","DOI":"10.1145\/3106237.3106309"},{"key":"397_CR36","unstructured":"Liu S (2018) Analysing timed traces using SMT solving. Master\u2019s thesis, University of Konstanz"},{"key":"397_CR37","unstructured":"Apache Software Foundation (2019) Maven, https:\/\/maven.apache.org\/"},{"key":"397_CR38","doi-asserted-by":"crossref","unstructured":"Milner R(1980) A calculus of communicating systems, volume\u00a092 of Lecture notes in computer science. Springer","DOI":"10.1007\/3-540-10235-3"},{"key":"397_CR39","unstructured":"opaal (2011). opaal test folder. http:\/\/opaal-modelchecker.com\/opaal-ltsmin\/. Accessed: 2018-11-08"},{"key":"397_CR40","unstructured":"Polsen DB, van Vliet J (2010) Concrete delays for symbolic traces. Master\u2019s thesis, Department of Computer Science, Aalborg University. Available from https:\/\/projekter.aau.dk\/projekter\/files\/32183338\/report.pdf"},{"key":"397_CR41","doi-asserted-by":"crossref","unstructured":"Reynolds A, Kuncak V, Tinelli C, Barrett C, Deters M (2017) Refutation-based synthesis in smt. Formal methods in system design, Feb","DOI":"10.1007\/s10703-017-0270-2"},{"key":"397_CR42","unstructured":"Brito T (2015) Uppaal elevator example. https:\/\/github.com\/tfbrito\/UPPAAL. Accessed: 2019-01-20"},{"key":"397_CR43","unstructured":"Uppaal (2017) Uppaal benchmarks. http:\/\/www.it.uu.se\/research\/group\/darts\/uppaal\/benchmarks\/#benchmarks. Accessed: 2019-01-20"},{"issue":"1\u20132","key":"397_CR44","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"Yovine S (1997) KRONOS: a verification tool for real-time systems. STTT 1(1\u20132):123\u2013133","journal-title":"STTT"},{"key":"397_CR45","doi-asserted-by":"crossref","unstructured":"Yi W, Pettersson P, Daniels M (1994) Automatic verification of real-time communicating systems by constraint-solving. In: FORTE, volume\u00a06 of IFIP conference proceedings, pp 243\u2013258. Chapman and Hall. Full version of the paper is available from http:\/\/www.it.uu.se\/research\/group\/darts\/papers\/texts\/wpd-forte94-full.pdf","DOI":"10.1007\/978-0-387-34878-0_18"},{"key":"397_CR46","unstructured":"Microsoft Research (2019) The Z3 Theorem Prover. https:\/\/github.com\/Z3Prover\/z3"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00397-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-022-00397-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00397-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,27]],"date-time":"2022-12-27T10:16:53Z","timestamp":1672136213000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-022-00397-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":46,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["397"],"URL":"https:\/\/doi.org\/10.1007\/s10703-022-00397-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12]]},"assertion":[{"value":"21 May 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 September 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 October 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"All authors consent to participate in the research described in this manuscript.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent to participate"}},{"value":"All authors and the institutions that they are affiliated with consent to the publication of the results contained in this manuscript.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for publication"}},{"value":"See above. The tool <scp>TarTar<\/scp> was successful in the artefact evaluation of the CAV 2020 conference, c.f. [].","order":5,"name":"Ethics","group":{"name":"EthicsHeading","label":"Code availability"}}]}}