I 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 reachability property. We present an encoding of TDTs in quantifier-free linear real arithmetic and use the minimal satisfiability core capabilities of the SMT solver Z3 to compute possible repairs. We then present an admissibility criterion, called functional equivalence, that assesses whether a proposed repair is admissible in the overall context of the NTA. I will then describe the architecture of a proof of concept tool called TarTar, which implements the analysis, repair and admissibility test that I describe. I will finally discuss the relationship of the analysis to causal reasoning in timed systems and present some experimental results.

This is joint work with Martin Koelbl (University of Konstanz) and Thomas Wies (New York University).