论文标题
视觉反例解释用于使用Oeritte进行模型检查
Visual counterexample explanation for model checking with Oeritte
论文作者
论文摘要
尽管是确保系统正确性的最可靠的方法之一，但模型检查仍需要辅助工具才能充分利用。在这项工作中，我们解决了其结果难以解释和呈现Oeritte的问题，这是一种自动视觉反例解释的工具。为了了解出了什么问题，用户可以检查违反的LTL公式的解析树和反例的表观，其中突出显示了重要的变量。然后，在验证的系统的功能框图上，他们可以在感兴趣的计算值与中间结果或功能框图的输入之间获得因果关系的可视化。因此，Oeritte有助于减少正式模型和规格调试工作，并使模型检查更具利用为复杂的工业系统。
Despite being one of the most reliable approaches for ensuring system correctness, model checking requires auxiliary tools to fully avail. In this work, we tackle the issue of its results being hard to interpret and present Oeritte, a tool for automatic visual counterexample explanation for function block diagrams. To learn what went wrong, the user can inspect a parse tree of the violated LTL formula and a table view of a counterexample, where important variables are highlighted. Then, on the function block diagram of the system under verification, they can receive a visualization of causality relationships between the calculated values of interest and intermediate results or inputs of the function block diagram. Thus, Oeritte serves to decrease formal model and specification debugging efforts along with making model checking more utilizable for complex industrial systems.
