Watchdog Transformations for Property-Oriented Model-Checking
Watchdog Transformations for Property-Oriented Model-Checking
复制标题
用于面向属性的模型检查的看门狗转换
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Irfan Zakiuddin
中科院分区：
文献类型：
--
作者：
M. Goldsmith;N. Moffat;B. Roscoe;Tim Whitworth;Irfan Zakiuddin
我们讨论了如何转换CSP细化，（S sqsubseteq I），使其所有事件都被隐藏；这很有用，因为模型检查器FDR提供的许多状态空间压缩函数只有在事件被隐藏时才有效。在较早的一篇论文[2]中，我们描述了一种适合于细化在CSP的跟踪语义中的情况的转换。本文将该方法扩展到更困难的稳定失效语义情况。在这两种情况下，将看门狗转换应用于规范S，从而产生看门狗processWDS，然后将其与I或在简单上下文中与I并行组合。看门狗进程监视I，并以某种方式指示它的行为是否与s的细化不兼容。原始断言的所有事件都可以隐藏在转换后的断言中。我们还讨论了压缩策略的设计，这些策略试图在I和WDS的组件进程中隐藏尽可能多的事件，并在构建组合时压缩组合。我们描述了看门狗转换的实现和一些简单的压缩策略。
We discuss how to transform a CSP refinement, (S sqsubseteq I), to enable all its events to be hidden; this is useful because many of the state space compression functions provided by the model-checker FDR are effective only when events are hidden [1]. In an earlier paper [2] we described a suitable transformation for the case where the refinement is in the traces semantics of CSP. This paper extends the approach to the more difficult case of the stable-failures semantics. In both cases, a watchdog transformation is applied to the specification S, resulting in a watchdog processWDS, which is then composed in parallel with I, or with I in a simple context. The watchdog process monitors I and somehow indicates whether it can behave in a way that is incompatible with refinement of S. All events of the original assertion can be hidden in the transformed assertion. We also discuss the design of compression strategies that try to hide as many events as possible in the component processes of I and WDS, and compress the composition as it is being built up. We describe our implementation of the watchdog transformations and some simple compression strategies.