LocFaults 可扩展性的探索
人工智能
2015-03-19 v1 软件工程
摘要
模型检查器可以为错误程序生成反例轨迹，该轨迹通常很长且难以理解。一般来说，在此轨迹中关于循环的部分是指令中最大的部分。这使得定位循环中的错误对于分析整个程序中的错误至关重要。在本文中，我们探索了 LocFaults（我们的错误定位方法）的可扩展性能力，该方法利用来自反例的控制流图（CFG）路径来计算 MCD（最小校正偏差），并从每个发现的 MCD 中计算 MCS（最小校正子集）。我们展示了该方法在展开 b 次的 While 循环程序以及偏差条件数量从 0 到 n 变化时的运行时间。我们的初步结果表明，与基于 SAT 并将整个程序转换为布尔公式的 BugAssist 相比，我们这种基于约束和流驱动的方法的时间性能更好，此外，LocFaults 提供的信息对用户更具表达力。
引用
@article{arxiv.1503.05530,
title = {Exploration of the scalability of LocFaults},
author = {Mohammed Bekkouche},
journal= {arXiv preprint arXiv:1503.05530},
year = {2015}
}
备注
in French