一种自动的形式化验证技术-模型检测

• 作者: 化志章 揭安全 薛锦云
• 来源期刊: 科技与创新
• 关键词: 模型检测 形式验证 时态逻辑
• 年，卷（期）: 2007,（33）
• 所属期刊栏目: 软件时空
• 页码范围: 254-256,222
• 页数: 4页
• 分类号: TP301.1
• 语种: 中文
• DOI: 10.3969/j.issn.1008-0570.2007.33.098

摘要

模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单介绍了软件模型检测的新进展.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	化志章		1	7	1.0	1.0
5	揭安全		1	7	1.0	1.0
9	薛锦云		1	7	1.0	1.0