How to Make FDR Spin LTL Model Checking of CSP by Refinement
How to Make FDR Spin LTL Model Checking of CSP by Refinement
复制标题
如何通过细化对CSP进行FDR Spin LTL模型检验
DOI：
10.1007/3-540-45251-6_6
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
A. Currie
中科院分区：
文献类型：
--
作者：
M. Leuschel;T. Massart;A. Currie
我们研究了在细化背景下对 CSP 规范进行 LTL 模型检查的可能性。我们提供的证据表明，基于细化的验证方法似乎不太适合验证某些时间属性。为了解决这个问题，我们展示了如何（以及如何不）使用一般的细化检查，特别是 FDR 工具来执行 CSP 流程的 LTL 模型检查。我们展示了如何处理（潜在的）死锁系统，讨论了我们的方法对于无限状态系统的有效性，并阐明了“经典”模型检查和细化检查之间的关系。
We study the possibility of doing LTL model checking on CSP specifications in the context of refinement. We present evidence that the refinement-based approach to verification does not seem to be very well suited for verifying certain temporal properties. To remedy this problem, we show how to (and how not to) perform LTL model checking of CSP processes using refinement checking in general and the FDR tool in particular. We show how one can handle (potentially) deadlocking systems, discuss the validity of our approach for infinite state systems, and shed light on the relationship between "classical" model checking and refinement checking.