Computer Science ›› 2015, Vol. 42 ›› Issue (7): 118-121.doi: 10.11896/j.issn.1002-137X.2015.07.025

Previous Articles     Next Articles

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: ion and Composition CHEN Dao-xi1 ZHANG Guang-quan2 XU Cheng-kai2 CHEN Guo-bin3 (Suzhou Senior Technician Institute,Suzhou 215009,China)1 (School of Computer Science & Technology,Soochow University,Suzhou 215006,China)2 (Rongzhi College,Chongqing Technology and Business University,Chongqing 400033,China)3 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

[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

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!