超性质的可视化分析：用于理解模型检测结果

模型检测器提供算法，用于证明系统的数学模型满足给定规范。在违反规范的情况下，会返回一个显示错误行为的反例。理解这些反例具有挑战性，特别是对于超性质规范（即关联系统多次执行的规范）。我们旨在通过我们的 HyperVis 工具促进此类反例的可视化分析，该工具提供给定模型、规范和反例的交互式可视化。在一个迭代且跨学科的设计过程中，我们开发了能够有效传达模型检测结果核心方面的可视化方案。具体而言，我们引入了二进制值的图形表示以改善模式识别，颜色编码以更好地指示相关方面，视觉增强的文本描述，以及广泛的交叉视图高亮机制。此外，通过对反例的底层因果分析，我们还能识别导致违反的值，并将此知识用于改进编码和高亮。最后，分析人员可以直接在 HyperVis 中修改超性质的规范和系统，并启动新版本的模型检测。综合来看，这些功能显著支持分析人员理解导致反例的错误以及迭代所提供的系统和规范。我们使用 HyperVis 进行了多个案例研究，并在定性反馈会议中与领域专家进行了测试。参与者的积极反馈证实了相对于手动的、基于文本的现状的显著改进，以及该工具在解释超性质方面的价值。