计算机科学 ›› 2015, Vol. 42 ›› Issue (7): 118-121.doi: 10.11896/j.issn.1002-137X.2015.07.025
陈道喜,张广泉,徐成凯,陈国彬
CHEN Daoxi, ZHANG Guangquan, XU Chengkai and CHEN Guobin
摘要: 由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。
[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! |
|