TarTar

Abstract:
We present algorithms and techniques for the repair of timed systemmodels, given as networks of timed automata (NTA). The repair is based on ananalysis of timed diagnostic traces (TDTs) that are computed by real-time modelchecking tools, such as UPPAAL, when they detect the violation of a timed safetyproperty. We present an encoding of TDTs in linear real arithmetic and use theMaxSMT capabilities of the SMT solver Z3 to compute possible repairs to clockbound values that minimize the necessary changes to the automaton. We thenpresent an admissibility criterion, called functional equivalence, that assesseswhether a proposed repair is admissible in the overall context of the NTA. Wehave implemented a proof-of-concept tool called TARTARfor the repair and ad-missibility analysis. To illustrate the method, we have considered a number ofcase studies taken from the literature and automatically injected changes to clockbounds to generate faulty mutations. Our technique is able to compute a feasiblerepair for91%of the faults detected by UPPAAL in the generated mutants.

Publications

• Martin Kölbl, Stefan Leue and Thomas Wies:  Clock Bound Repair for Timed Systems. In: Computer Aided Verification - 31th International Conference, CAV 2019, 79-96.
  Download: [pdf]