%0 Journal Article
%T 基于抽象和组合方法的网络协议验证
%A 陈道喜？
%A 张广泉？
%A 徐成凯？
%A 陈国彬？
%J 计算机科学
%D 2015
%R 10.11896/j.issn.1002-137X.2015.07.025
%X 由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的ltl性质,建立各个通信主体的kripke结构,再对该kripke结构进行抽象；然后组合抽象模型；最后运用spin对组合抽象模型进行检验。为验证该方法的有效性,对nspk协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。
%K kripke结构
%K 状态爆炸
%K 组合抽象模型
%K ltl模型检测
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=20150725&flag=1