TarTar: A Timed Automata Repair Tool
This addresses the need for efficient model repair in timed systems, offering a practical tool for engineers, though it is incremental as it builds on existing repair concepts.
The authors tackled the problem of automatically repairing timed automata models by presenting TarTar, a tool that suggests syntactic repairs to eliminate timed diagnostic traces while preserving system behavior, achieving a 69% success rate on seeded errors across diverse case studies.
We present TarTar, an automatic repair analysis tool that, given a timed diagnostic trace (TDT) obtained during the model checking of a timed automaton model, suggests possible syntactic repairs of the analyzed model. The suggested repairs include modified values for clock bounds in location invariants and transition guards, adding or removing clock resets, etc. The proposed repairs are guaranteed to eliminate executability of the given TDT, while preserving the overall functional behavior of the system. We give insights into the design and architecture of TarTar, and show that it can successfully repair 69% of the seeded errors in system models taken from a diverse suite of case studies.