ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sun 7 Apr 2019 16:00 - 16:45 at S6 - Causality, repairs and multi-agent systems

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).

Analysis, Repair and Causality for Timed Diagnostic Traces (Stefan Leue.pdf)1.29MiB

Sun 7 Apr