反例引导的模型检验工具的设计

摘要：

针对模型组合中常见的"状态空间爆炸"问题,分析了抽象和组合两种方法各自的优缺点,采用"反例引导的抽象精化"框架和模型检验思想,将抽象和组合结合起来,为模型组合的检验提出了一种新的方法.设计了模型的抽象、组合、检验和精化算法,开发了一款基于反例引导的、图形化的模型检验工具,使用Kripke结构建立模型,用LTL描述性质,从而表明了反例引导的模型检验方法的过程.

关键词：模型检验、状态爆炸、反例引导、抽象精化、抽象与组合

所属期刊栏目：30

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

资助基金：国家自然科学基金项目60673115;上海市重点学科建设基金项目J50103

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

页数：共4页

页码：5041-5043,5047