A formal verification method: model checking(一种形式化验证方法：模型检验)

A formal verification method: model checking(一种形式化验证方法：模型检验)

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

Full description

Bibliographic Details
Main Authors: YANGJun(杨军), GEHai-tong(葛海通), ZHENGFei-jun(郑飞君), YANXiao-lang(严晓浪)
Format: Article
Language:zho
Published: Zhejiang University Press 2006-07-01
Series:Zhejiang Daxue xuebao. Lixue ban
Subjects:
模型检验
kripke结构
ctl逻辑
标记
固定点
符号模型检验
Online Access:https://doi.org/zjup/1008-9497.2006.33.4.403-407
Description
Summary:模型检验作为一种形式化验证方法，近年来在各种硬件、软件设计中得到了广泛应用.文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑，然后介绍了模型检验中常用的两种算法：标记算法和基于固定点的算法，最后介绍了为避免内存爆炸而引入的符号模型检验技术.
ISSN:1008-9497

Similar Items