@inproceedings{968895d7f7724a8ab2fe8d7a0481864e,
title = "Clock Bound Repair for Timed Systems",
abstract = "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 compute possible repairs to clock bound values that minimize the necessary changes to the automaton. We then present an admissibility criterion, called functional equivalence, that assesses whether a proposed repair is admissible in the overall context of the NTA. We have implemented a proof-of-concept tool called TarTar for the repair and admissibility analysis. To illustrate the method, we have considered a number of case studies taken from the literature and automatically injected changes to clock bounds to generate faulty mutations. Our technique is able to compute a feasible repair for 91 of the faults detected by UPPAAL in the generated mutants.",
keywords = "Admissibility of repair, Automated repair, TarTar tool, Timed automata",
author = "Martin K{\"o}lbl and Stefan Leue and Thomas Wies",
note = "Publisher Copyright: {\textcopyright} The Author(s). 2019.; 31st International Conference on Computer Aided Verification, CAV 2019 ; Conference date: 15-07-2019 Through 18-07-2019",
year = "2019",
doi = "10.1007/978-3-030-25540-4_5",
language = "English (US)",
isbn = "9783030255398",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "79--96",
editor = "Isil Dillig and Serdar Tasiran",
booktitle = "Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings",
}