基于抽象和组合方法的网络协议验证

由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象；然后组合抽象模型；最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。

Verification of Network Protocols Based on Abstraction and Composition

ion and Composition CHEN Dao-xi¹ ZHANG Guang-quan² XU Cheng-kai² CHEN Guo-bin³ (Suzhou Senior Technician Institute,Suzhou 215009,China)¹ (School of Computer Science & Technology,Soochow University,Suzhou 215006,China)² (Rongzhi College,Chongqing Technology and Business University,Chongqing 400033,China)³ Abstract 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.