文献类型：期刊文章

作　　者：杨军[1] 葛海通[1] 郑飞君[1] 严晓浪[1]

机构地区：[1]浙江大学超大规模集成电路设计研究所,浙江杭州310027

出　　处：《浙江大学学报（理学版）》

基　　金：国家自然科学基金资助项目(No.90207002)

年　　份：2006

卷　　号：33

期　　号：4

起止页码：403-407

语　　种：中文

收录情况：AJ、BDHX、BDHX2004、CAB、CAS、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、IC、JST、MR、PROQUEST、RCCSE、SCOPUS、WOS、ZGKJHX、ZMATH、ZR、核心刊

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

关 键 词：模型检验  KRIPKE结构 CTL逻辑  标记  固定点 符号模型检验

分 类 号：TP301]