Reachability analysis has proved to be one of the most effective methods in verifying correctness of communication protocols based on the state transition model. Consequently, many protocol verification tools have been built based on the method of reachability analysis. Nevertheless, it is also well known that state space explosion is the most severe limitation to the applicability of this method. Although researchers in the field have proposed various strategies to relieve this intricate problem when building the tools, a survey and evaluation of these strategies has not been done in the literature. In searching for an appropriate approach to tackling such a problem for a grammar-based validation tool, we have collected and evaluated these relief strategies, and have decided to develop our own from yet another but more systematic approach. The results of our research are now reported in this paper. Essentially, the paper is to serve two purposes: first, to give a survey and evaluation of existing relief strategies; second, to propose a new strategy, called PROVAT (PROtocol VAlidation Testing), which is inspired by the heuristic search techniques in Artificial Intelligence. Preliminary results of incorporating the PROVAT strategy into our validation tool are reviewed in the paper. These results show the empirical evidence of the effectiveness of the PROVAT strategy.
可证明性分析已被证明是验证基于状态转移模型的通信协议正确性的最有效方法之一。因此,基于可达性分析的方法已经建立了许多协议验证工具。但是,众所周知,状态空间爆炸是此方法适用性的最严重限制。尽管该领域的研究人员已经提出了各种策略来缓解构建工具时的复杂问题,但是文献中尚未对这些策略进行调查和评估。在寻找适当的方法来解决基于语法的验证工具中的此类问题时,我们收集并评估了这些缓解策略,并决定从另一种但更系统的方法中开发自己的方法。现在,我们的研究结果已在本文中进行了报道。从本质上讲,本文旨在达到两个目的:第一,对现有救济策略进行调查和评估;其次,提出一种称为PROVAT(协议验证测试)的新策略,该策略受到人工智能中启发式搜索技术的启发。本文回顾了将PROVAT策略纳入我们的验证工具的初步结果。这些结果证明了PROVAT策略的有效性。 P>
Ohio State Univ., Columbus, OH;
机译:使用缩窄的符号可达性分析及其在密码协议验证中的应用
机译:使用QDD对具有无限状态空间的通信协议进行符号验证
机译:上肢的可再生性分析到达工作空间,以及采集协议,性别和手中占主导地位的影响
机译:基于概率可达性分析的通信协议属性验证
机译:探索甚至可达的全局状态空间以验证协议的死锁自由度。
机译:Sentinel淋巴结中的转移检测:有限的广泛间隔(NSABP协议B-32)的比较以及综合狭窄的石蜡区块切片策略
机译:使用缩小的符号可及性分析及其在密码协议验证中的应用