一种形式化验证方法:模型检验

• 作者: 严晓浪 杨军 葛海通 郑飞君
• 来源期刊: 浙江大学学报（理学版）
• 学科: 工学
• 关键词: 模型检验 Kripke结构 CTL逻辑 标记 固定点 符号模型检验
• 年，卷（期）: 2006,（4）
• 所属期刊栏目: 电子科学
• 页码范围: 403-407
• 页数: 5页
• 分类号: TP301
• 字数: 5139字
• 语种: 中文
• DOI: 10.3321/j.issn:1008-9497.2006.04.012

摘要

模型检验作为一种形式化验证方法,近年来在各种硬件、软件设计中得到了广泛应用.文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑,然后介绍了模型检验中常用的两种算法:标记算法和基于固定点的算法,最后介绍了为避免内存爆炸而引入的符号模型检验技术.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨军	浙江大学超大规模集成电路设计研究所	59	513	11.0	19.0
2	严晓浪	浙江大学超大规模集成电路设计研究所	246	1634	19.0	29.0
3	葛海通	浙江大学超大规模集成电路设计研究所	52	293	8.0	14.0
4	郑飞君	浙江大学超大规模集成电路设计研究所	8	114	5.0	8.0