An Automated Approach for the Interpretation of Counter-Examples
An Automated Approach for the Interpretation of Counter-Examples
复制标题
解释反例的自动化方法
DOI：
10.1016/j.entcs.2006.12.027
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Wendy Johnston
中科院分区：
文献类型：
--
作者：
L. V. D. Berg;P. Strooper;Wendy Johnston
模型检查是一种用于验证有限系统的自动技术。模型检查器探索给定模型的完整状态空间，并根据一组需求对其进行检查。如果存在不满足要求的状态，大多数工具都会生成反例。反例对于调试模型和确定建模系统中是否存在错误非常有用。然而，最终用户可能很难理解它们，这可能会限制模型检查在行业中的应用。本文描述了一种特定领域的方法来自动解释反例并以直观的形式向最终用户呈现结果。我们的研究扩展了之前与昆士兰铁路信号工程师一起进行铁路信号控制表模型检查的工作。
Model checking is an automatic technique used for the verification of finite systems. A model checker explores the full state space of a given model and checks it against a set of requirements. If a state exists in which a requirement is not satisfied most tools will generate a counter-example. Counter-examples are useful for debugging a model and determining if an error exists in the modelled system. However, they can be difficult for end users to understand and this may limit the take-up of model checking in industry. This paper describes a domain-specific approach to automatically interpreting counter-examples and presenting the results in an intuitive form to the end user. Our research extends previous work on model checking railway signalling control tables with signalling engineers from Queensland Rail.