Trace Abstraction Refinement for Timed Automata
Trace Abstraction Refinement for Timed Automata
复制标题
定时自动机的迹线抽象细化
DOI：
10.1007/978-3-319-11936-6_28
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
L. Jiao
中科院分区：
文献类型：
--
作者：
Weifeng Wang;L. Jiao
定时自动机是一种众所周知的实时系统建模形式。定时自动机的模型检查对于确保系统满足某些属性非常重要。安全性是定时自动机最重要的属性之一。在本文中，我们提出了一种用于时间自动机安全检查的方法，该方法是通用跟踪抽象细化框架对时间自动机的适应。我们工作的特点是我们使用基于区域的 LU 抽象而不是插值技术。该方法仅在必要时执行区域计算，并且区域的抽象较粗，因为在计算 LU-bounds 时仅考虑部分控制结构。我们举一个例子来说明这种方法何时可以比传统的基于区域的搜索算法更有效地执行。
Timed automata are a well known formalism for modeling real-time systems. Model checking of timed automata is important for ensuring that the systems satisfy certain properties. Safety is one of the most important properties for timed automata. In this paper we propose a method for the safety checking of timed automata, which is an adaptation of the general trace abstraction refinement framework to timed automata. The feature of our work is that we use zone-based LU-abstraction instead of interpolation techniques. This method performs zone computation only when necessary, and the abstraction on zones is coarser because only part of the control structure is considered when computing LU-bounds. We give an example to show when this method could perform more efficiently than the traditional zone-based search algorithm.