A formal verification method: model checking(一种形式化验证方法：模型检验)
模型检验作为一种形式化验证方法，近年来在各种硬件、软件设计中得到了广泛应用.文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑，然后介绍了模型检验中常用的两种算法：标记算法和基于固定点的算法，最后介绍了为避免内存爆炸而引入的符号模型检验技术....
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | zho |
| Published: |
Zhejiang University Press
2006-07-01
|
| Series: | Zhejiang Daxue xuebao. Lixue ban |
| Subjects: | |
| Online Access: | https://doi.org/zjup/1008-9497.2006.33.4.403-407 |
| _version_ | 1797236277143142400 |
|---|---|
| author | YANGJun(杨军) GEHai-tong(葛海通) ZHENGFei-jun(郑飞君) YANXiao-lang(严晓浪) |
| author_facet | YANGJun(杨军) GEHai-tong(葛海通) ZHENGFei-jun(郑飞君) YANXiao-lang(严晓浪) |
| author_sort | YANGJun(杨军) |
| collection | DOAJ |
| description | 模型检验作为一种形式化验证方法，近年来在各种硬件、软件设计中得到了广泛应用.文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑，然后介绍了模型检验中常用的两种算法：标记算法和基于固定点的算法，最后介绍了为避免内存爆炸而引入的符号模型检验技术. |
| first_indexed | 2024-04-24T17:01:18Z |
| format | Article |
| id | doaj.art-18d6c86e13404c48be7f131e68c9457e |
| institution | Directory Open Access Journal |
| issn | 1008-9497 |
| language | zho |
| last_indexed | 2024-04-24T17:01:18Z |
| publishDate | 2006-07-01 |
| publisher | Zhejiang University Press |
| record_format | Article |
| series | Zhejiang Daxue xuebao. Lixue ban |
| spelling | doaj.art-18d6c86e13404c48be7f131e68c9457e2024-03-29T01:58:23ZzhoZhejiang University PressZhejiang Daxue xuebao. Lixue ban1008-94972006-07-01334403407zjup/1008-9497.2006.33.4.403-407A formal verification method: model checking(一种形式化验证方法：模型检验)YANGJun(杨军)0GEHai-tong(葛海通)1ZHENGFei-jun(郑飞君)2YANXiao-lang(严晓浪)3Institute of VLSI Design, Zhejiang University, Hangzhou 310027, China(浙江大学超大规模集成电路设计研究所，浙江 杭州 310027)Institute of VLSI Design, Zhejiang University, Hangzhou 310027, China(浙江大学超大规模集成电路设计研究所，浙江 杭州 310027)Institute of VLSI Design, Zhejiang University, Hangzhou 310027, China(浙江大学超大规模集成电路设计研究所，浙江 杭州 310027)Institute of VLSI Design, Zhejiang University, Hangzhou 310027, China(浙江大学超大规模集成电路设计研究所，浙江 杭州 310027)模型检验作为一种形式化验证方法，近年来在各种硬件、软件设计中得到了广泛应用.文中首先介绍了描述系统行为的Kripke结构和描述系统性质的CTL逻辑，然后介绍了模型检验中常用的两种算法：标记算法和基于固定点的算法，最后介绍了为避免内存爆炸而引入的符号模型检验技术.https://doi.org/zjup/1008-9497.2006.33.4.403-407模型检验kripke结构ctl逻辑标记固定点符号模型检验 |
| spellingShingle | YANGJun(杨军) GEHai-tong(葛海通) ZHENGFei-jun(郑飞君) YANXiao-lang(严晓浪) A formal verification method: model checking(一种形式化验证方法：模型检验) Zhejiang Daxue xuebao. Lixue ban 模型检验 kripke结构 ctl逻辑 标记 固定点 符号模型检验 |
| title | A formal verification method: model checking(一种形式化验证方法：模型检验) |
| title_full | A formal verification method: model checking(一种形式化验证方法：模型检验) |
| title_fullStr | A formal verification method: model checking(一种形式化验证方法：模型检验) |
| title_full_unstemmed | A formal verification method: model checking(一种形式化验证方法：模型检验) |
| title_short | A formal verification method: model checking(一种形式化验证方法：模型检验) |
| title_sort | formal verification method model checking 一种形式化验证方法 模型检验 |
| topic | 模型检验 kripke结构 ctl逻辑 标记 固定点 符号模型检验 |
| url | https://doi.org/zjup/1008-9497.2006.33.4.403-407 |
| work_keys_str_mv | AT yangjunyángjūn aformalverificationmethodmodelcheckingyīzhǒngxíngshìhuàyànzhèngfāngfǎmóxíngjiǎnyàn AT gehaitonggéhǎitōng aformalverificationmethodmodelcheckingyīzhǒngxíngshìhuàyànzhèngfāngfǎmóxíngjiǎnyàn AT zhengfeijunzhèngfēijūn aformalverificationmethodmodelcheckingyīzhǒngxíngshìhuàyànzhèngfāngfǎmóxíngjiǎnyàn AT yanxiaolangyánxiǎolàng aformalverificationmethodmodelcheckingyīzhǒngxíngshìhuàyànzhèngfāngfǎmóxíngjiǎnyàn AT yangjunyángjūn formalverificationmethodmodelcheckingyīzhǒngxíngshìhuàyànzhèngfāngfǎmóxíngjiǎnyàn AT gehaitonggéhǎitōng formalverificationmethodmodelcheckingyīzhǒngxíngshìhuàyànzhèngfāngfǎmóxíngjiǎnyàn AT zhengfeijunzhèngfēijūn formalverificationmethodmodelcheckingyīzhǒngxíngshìhuàyànzhèngfāngfǎmóxíngjiǎnyàn AT yanxiaolangyánxiǎolàng formalverificationmethodmodelcheckingyīzhǒngxíngshìhuàyànzhèngfāngfǎmóxíngjiǎnyàn |