摘要
由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。
Due to the state explosion problem in model checking,it is always impossible to verify the composition model of a multi-agent protocol.To relieve this problem,we analyzed the impact of the increase in the number of agents on that of states and then proposed an approach based on abstraction and composition.Firstly,Kripke structures of individual agents are established according to the LTL properties to be verified,and these structures are abstracted.Then,these abstraction models are composed.Finally,the tool Spin is used to verified the composed model.To validate the efficiency of this approach,we verified the protocol NSPK.The results show that there are significant decreases in the length of state-vector,depth searched and the number of states stored and transitions,which will help relieve the state explosion problem.
出处
《计算机科学》
CSCD
北大核心
2015年第7期118-121,共4页
Computer Science
基金
江苏省自然科学基金(BK2011281)
苏州市应用基础研究计划(SYG201241)
江苏省普通高校研究生科研创新计划(CXLX13_820)
重庆市教委科学技术研究项目(KJ133103)资助