反例分类
软件工程
2021-10-12 v3 形式语言与自动机理论
摘要
在模型检测中，当给定模型不满足期望的规约时，典型的模型检测器会提供一个反例来说明违反是如何发生的。一般而言，存在许多展现不同违反行为的多样化反例，用户可能希望在决定如何修复模型之前对这些反例进行考察。遗憾的是，在现有模型检测器中获取这一信息颇具挑战，因为（1）反例数量可能过于庞大而无法逐一枚举，且（2）其中许多反例是冗余的，因为它们描述了同一类型的违反行为。本文提出一种称为反例分类的技术。分类的目标是将所有反例的空间划分为有限个反例类，每一类描述给定规约下一种不同的违反行为类型。随后将这些类作为系统中可能违反行为的摘要呈现给用户，使用户无需手动检查或分析大量反例以提取相同信息。我们在现有的形式化建模与验证工具Alloy Analyzer之上实现了该技术的原型，并在涉及著名的Needham-Schroeder协议的案例研究中评估了该技术有效性，结果令人鼓舞。
引用
@article{arxiv.2108.00885,
title = {Counterexample Classification},
author = {Cole Vick and Eunsuk Kang and Stavros Tripakis},
journal= {arXiv preprint arXiv:2108.00885},
year = {2021}
}