并发反应式系统的组合模型检验与组合精化检验

摘要：

模型检验和精化检验是两种重要的形式验证方法,其应用的主要困难在于如何缓解状态爆炸问题.基于分而治之的思想进行组合模型检验和组合精化检验是应对这个问题的重要方法,它们利用系统的组合结构对问题进行分解,通过对各子系统性质的检验和综合推理导出整个系统的性质.在一个统一的框架下对组合模型检验和组合精化检验作了系统的分析和归纳,从模块检验的角度阐述了上述两种组合验证方法的原理及其相应的组合验证策略.同时总结了各类问题的复杂性,并对上述两种方法作了比较分析,揭示了它们之间的内在联系.最后展望了组合模型检验与组合精化检验的发展方向.

关键词：模型检验、精化检验、组合模型检验、组合精化检验、状态爆炸问题、模块检验

所属期刊栏目：18

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金60233020;60673118;90612009;国家高技术研究发展计划863计划2005AA113130;2006AA01Z429;国家重点基础研究发展计划973计划2005CB321802;教育部跨世纪优秀人才培养计划NCET-04-0996

在线出版日期：2007-07-23（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：1270-1281