基于Oeritte的模型检测可视化反例解释
系统与控制
2021-01-01 v1 人机交互
系统与控制
摘要
尽管模型检测是确保系统正确性最可靠的方法之一，它仍需辅助工具才能充分发挥作用。本文中，我们解决其结果难以解释的问题，并介绍Oeritte，一个用于功能块图自动可视化反例解释的工具。为弄清出错之处，用户可检查被违反的LTL公式的解析树以及反例的表格视图，其中重要变量被高亮。随后，在待验证系统的功能块图上，他们可获得所关注计算值与功能块图中间结果或输入之间因果关系的可视化。因此，Oeritte有助于减少形式化模型与规约的调试工作量，并使模型检测对复杂工业系统更易用。
引用
@article{arxiv.2012.15097,
title = {Visual counterexample explanation for model checking with Oeritte},
author = {Polina Ovsiannikova and Igor Buzhinsky and Antti Pakonen and Valeriy Vyatkin},
journal= {arXiv preprint arXiv:2012.15097},
year = {2021}
}
备注
The 25th International Conference on Engineering of Complex Computer Systems (ICECCS 2020)