论文标题
牙垢：定时自动机修复工具
TarTar: A Timed Automata Repair Tool
论文作者
论文摘要
我们提出了塔塔尔（Tartar），这是一种自动修复分析工具，鉴于在定时自动机模型的模型检查期间获得的定时诊断迹线（TDT），提出了分析模型的句法修复。建议的维修包括位置不变和过渡护罩中时钟边界的修改值，添加或删除时钟重置等。确保所提出的维修可以消除给定TDT的可执行性，同时保留系统的整体功能行为。我们对塔塔尔的设计和建筑有深入的了解，并表明它可以成功修复从各种案例研究中采取的系统模型中69％的种子错误。
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.
