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

• 作者: 曾红卫 谭亮
• 来源期刊: 计算机工程与设计
• 学科: 工学
• 关键词: 模型检验 状态爆炸 反例引导 抽象精化 抽象与组合
• 年，卷（期）: 2009,（22）
• 所属期刊栏目: 软件与算法
• 页码范围: 5041-5043,5047
• 页数: 4页
• 分类号: TP311
• 字数: 4081字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	曾红卫	上海大学计算机工程与科学学院	31	341	11.0	17.0
2	谭亮	上海大学计算机工程与科学学院	2	7	1.0	2.0