AI 中文总结
该研究针对定量自动机分析算法难验证问题，提出一个能生成非退化随机定量自动机、测试并缩小违规到局部最小值的框架，将其应用于PTA的IMITATOR模型检查器，发现5个未知错误，其中一个由简单反例暴露。
AI 中文摘要
定量自动机的分析算法复杂且难以验证。现有方法，如基准测试、变异测试、均匀随机生成，都无法发现细微的实现错误。我们提出了一个框架，该框架通过重复：1）生成构造上非退化的随机定量自动机；2）针对目标属性对每个自动机进行测试；3）将任何违规情况缩小到局部最小值，从而产生一个小的、可操作的反例。我们为参数化定时自动机（PTA）实现了该框架，并将其应用于成熟的PTA模型检查器IMITATOR，发现了5个以前未知的错误，其中一个错误由仅具有2个位置和1个转换的反例暴露。
英文摘要
Analysis algorithms for quantitative automata are complex and hard to validate. Existing approaches -- benchmarks, mutation testing, uniform random generation -- each fail to expose subtle implementation bugs. We present a framework that repeatedly 1) generates random quantitative automata that are non-degenerate by construction, 2) tests each against a target property, and 3) shrinks any violation to a local minimum, yielding a small, actionable counterexample. We implement the framework for parametric timed automata (PTA) and apply it to IMITATOR, a mature model checker for PTA, uncovering 5 previously unknown bugs, one of which was exposed by a counterexample with just 2 locations and 1 transition.
CommentsSubmitted version. Published version available at doi.org/10.1007/978-3-032-30693-7_13
Journal refTheoretical Aspects of Software Engineering (TASE 2026), Lecture Notes in Computer Science, vol. 16697, Springer, pp. 188-205, 2026
DOI：10.1007/978-3-032-30693-7_13
