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

作者：杨军; 葛海通; 郑飞君; 严晓浪

来源：浙江大学学报(理学版), 2006, (04): 403-407.

DOI：10.3321/j.issn:1008-9497.2006.04.012

• 模型检验
• Kripke结构
• CTL逻辑
• 标记
• 固定点
• 符号模型检验

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

• 单位
  浙江大学