摘要
模型检验作为一种形式化验证方法,近年来在各种硬件、软件设计中得到了广泛应用.文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑,然后介绍了模型检验中常用的两种算法:标记算法和基于固定点的算法,最后介绍了为避免内存爆炸而引入的符号模型检验技术.
Being a formal verification method, model checking is used frequently in hardware and software design. Firstey the Kripke structure which is used to describe the behavior of a system and the CTL logic which is used to describe the property of a system were introduced. Then two model checking algorithms were introduced： one is the labeling algorithm. the other is the algorithm based on fixpoint. In the end. the symbolic model checking which can reduce the possibility of memory explosion was introduced.
出处
《浙江大学学报（理学版）》
CAS
CSCD
北大核心
2006年第4期403-407,共5页
Journal of Zhejiang University（Science Edition）
基金
国家自然科学基金资助项目(No.90207002)
