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

doi:10.11896/j.issn.1002-137X.2015.07.025

计算机科学 ›› 2015, Vol. 42 ›› Issue (7): 118-121.doi: 10.11896/j.issn.1002-137X.2015.07.025

• 2014’全国理论计算机科学年会 • 上一篇下一篇

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

陈道喜,张广泉,徐成凯,陈国彬

苏州技师学院苏州215009,苏州大学计算机科学与技术学院苏州215006,苏州大学计算机科学与技术学院苏州215006,重庆工商大学融智学院重庆400033

出版日期:2018-11-14 发布日期:2018-11-14
基金资助:
本文受江苏省自然科学基金(BK2011281),苏州市应用基础研究计划(SYG201241),江苏省普通高校研究生科研创新计划(CXLX13_820),重庆市教委科学技术研究项目(KJ133103)资助

Verification of Network Protocols Based on Abstraction and Composition

CHEN Daoxi, ZHANG Guangquan, XU Chengkai and CHEN Guobin

Online:2018-11-14 Published:2018-11-14

摘要/Abstract

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

关键词: Kripke结构,状态爆炸,组合抽象模型,LTL模型检测

Abstract: 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.

Key words: Kripke structure,State explosion,Composition abstraction model,LTL model checking

陈道喜,张广泉,徐成凯,陈国彬. 基于抽象和组合方法的网络协议验证[J]. 计算机科学, 2015, 42(7): 118-121. https://doi.org/10.11896/j.issn.1002-137X.2015.07.025

CHEN Daoxi, ZHANG Guangquan, XU Chengkai and CHEN Guobin. Verification of Network Protocols Based on Abstraction and Composition[J]. Computer Science, 2015, 42(7): 118-121. https://doi.org/10.11896/j.issn.1002-137X.2015.07.025

参考文献

[1] Edmund M C,Oran G,Doron A P.Model Checking [M].Cambridge:MIT Press,1999
[2] 林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30(12A):1907-1912 Lin Hui-min,Zhang Wen-hui.Model Checking:Theories,Techniques and Applications[J].Acta Electronica Sinica,2002,30(12A):1907-1912
[3] Edmund M C,Oran G,David E L.Model checking and abstraction [J].ACM Transactions on Programming Languages and Systems,1994,16(5):1512-1542
[4] 刘志锋,孙博,周从华.概率实时时态认知逻辑模型检测中抽象技术的研究[J].电子学报,2013,41(7):1343-1351 Liu Zhi-feng,Sun Bo,Zhou Cong-hua.Abstraction in Model Checking Probabilistic Real-Time Temporal Logic of Know-ledge[J].Acat Electronica Sinica,2013,41(7):1343-1351
[5] Grumberg O,Vardi M Y,Sifakis J,et al.2010 CAV award announcement[J].Formal Methods in System Design,2012,40(2):117-120
[6] Mendoza L E,Capel M I,Perez M A.Conceptual framework for business processes compositional verification [J].Information and software technology,2012,54(2):149-161
[7] 曾红卫,缪淮扣.构件组合的抽象精化验证 [J].软件学报,2008,9(5):1149-1159 Zeng Hong-Wei,Miao Huai-Kou.Verification of Component Composition Based on Abstraction Refinement[J].Journal of Software,2008,9(5):1149-1159
[8] Carbone R.LTL model-checking for security protocols[J].AI communications,2011,24(3):385-396
[9] 高建华,蒋颖.基于余归纳的最小Kripke结构的求解[J].软件学报,2014,25(1):16-26 Gao Jian-hua,Jiang Ying.Coinduction-Based Solution for Minimization of Kripke Structures[J].Journal of Software,2014,25(1):16-26
[10] Gerard J H.The SPIN Model Checker:Primer and ReferenceManual [M].Boston:Addison-Wesley,2004
[11] 吕威,黄志球,陈哲,等.ESpin:基于 SPIN 的 Eclipse模型检测环境[J].计算机工程与应用,2013,49(7):45-51 Lv Wei,Huang Zhi-qiu,Chen Zhe,et al.ESpin:SPIN-based Eclipse model checking environment[J].Computer Engineering and Applications,2013,49(7):45-51
[12] Patig S,Stolz M.A pattern-based approach for the verification of business process descriptions[J].Information and Software Technology,2013,55(1):58-87
[13] Ikeda,Satoshi,Jibiki,et al.Coverage Estimation in Model Checking with Bitstate Hashing[J].IEEE Transactions on Software Engineering,2013,39(4):477-486

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

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

Verification of Network Protocols Based on Abstraction and Composition

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 0

Metrics

本文评价

推荐阅读 0