Paper on Automated Repair of Timed Systems Accepted for CAV 2019
The paper "Clock Bound Repair for Timed Systems", authored by Martin Kölbl, Stefan Leue and Thomas Wies (New York University) has been accepted for the 31st International Conference on Computer-Aided Verification CAV 2019, to be held in New York City in July, 2019.
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 theviolation of a timed safety property. We present an encoding ofTDTs in linear real arithmetic and use the MaxSMT capabilities of the SMT solver Z3 to computepossible 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 andautomatically injected changes to clock bounds to generate faulty mutations. Our technique is able to compute a feasible repair for 90% of the faults detected by UPPAALin the generated mutants.