一种改进的大规模CTL公式检测算法.pdfVIP

第40卷 第 10期 计 算 机 科 学 Vo1．40No．10 2013年 10月 Computer Science Oct2013 一 种改进的大规模 CTL公式检测算法 奚 琪 王清贤 曾勇军 秦艳锋 (国家数字交换系统工程技术研究中心 郑州450002) 摘 要 标记算法是模型检测用于验证计算树逻辑CTL公式的经典算法。针对标记算法检测大规模公式存在的效 率问题，提 出一种可用于验证大规模CTL公式的标记算法。算法通过公式预处理标识公式集中的公共子公式，在验 证过程中绑定公共子公式与模型状态，避免公式的重复验证 。实验结果表明，该算法有效提高了验证效率。 关键词 模型检测，标记算法，公共子公式，语法分析树 中图法分类号 TP309 文献标识码 A ImprovedAlgorithm forLarge-scaleCTL FormulaeVerification Ⅺ Qi WANGQing-xian ZENGYong-jun QINYan-feng (ChinaNationalDigitalSwitchingSystem EngineeringandTechnologicalResearchCenter，Zhengzhou450002，China) Abstract Labellingalgorithm isastandardalgoritmh formodelcheckingCTLformulas．Thispaperpresentedanalgo- rithm toimproveefficiencyforlarge-scaleCTLformulasverification．Itidentifiescommon subformulasfrom fomr ulae set，bindingprogram stateswithlabdsofcommonsubformulastoavoidrepeatingcheckingthem．Theexperimentalre— suhsillustratetheadvantagesontheefficiencyofthenew algorithm． Keywords Modalchecking ，Labdling algorithm，Commonsubfomr ulas，Parsetree 证的方法，这种不考虑公式相似性的验证方法效率低下，无法 1 引言 满足现实的验证需求。 随着计算机软硬件的规模与复杂性不断增大 ，提高系统 本文在标记算法的基础上提出了一种验证大规模 CTL 正确性和可靠性的验证技术 日益受到重视 。在诸多的验证方 公式 的模型检测算法 LsLA(LargeScaleLabelling Algo— 法之中，模型检测以其 自动化程度高、实用性强受到广泛关 rithm)。算法首先通过公式预处理标识出公式集中的所有公 注。目前模型检测已在硬件设计、通信协议等领域得到广泛 共子公式 ，对公式进行合并生成CTL公式集语法树。模型检 应用，并在软件安全领域也有很大进展。 测过程中通过绑定公共子公式及其在模型中可满足的状态， Clarke[1]等提 出利用计算树逻辑 (ComputationTree 克服重复验证公共子公式的问题。实验说明该算法可有效提 Logic，CTL)描述并发系统的性质，设计实现了检验有穷状态 高大规模CTL公式的验证效率。 系统是否满足给定CTL公式的标记算法[2]，这为 自动化验证 2 问题提出 并发系统性质奠定 了基础。文献E3]提出的EMC算法能够 提高检测模型的