| 一种自动的形式化验证技术-模型检测 |
| |
| 引用本文： | 化志章,揭安全,薛锦云.一种自动的形式化验证技术-模型检测[J].微计算机信息,2007,23(33):254-256,222. |
| |
| 作者姓名： | 化志章 揭安全 薛锦云 |
| |
| 作者单位： | 330022,南昌江西省 高性能计算技术重点实验室;330022,南昌 江西师范大学计算机信息工程学院 |
| |
| 基金项目： | 国家重大基础研究前期研究专项(973计划);国家自然科学基金;江西省教育厅科研项目 |
| |
| 摘 要： | 模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单介绍了软件模型检测的新进展.
|
| 关 键 词： | 模型检测 形式验证 时态逻辑 |
| 文章编号： | 1008-0570（2007）11-3-0254-03 |
| 修稿时间： | 2007-09-032007-10-05 |
Model-Checking-An Automatic Formal Verification Technique |
| |
| HUA ZHIZHANG,JIE ANQUAN,XUE JINYUN.Model-Checking-An Automatic Formal Verification Technique[J].Control & Automation,2007,23(33):254-256,222. |
| |
| Authors: | HUA ZHIZHANG JIE ANQUAN XUE JINYUN |
| |
| Affiliation: | Key Lab For High-Performance Computing Technology Jiang Xi Province, Jiang Xi, Nan Chang, 330022;College of Computer Information and Engineering, Jiangxi Normal University, Jiang Xi, Nanchang 330022 |
| |
| Abstract: | Model checking is a technique of automatically verifying logical properties of the behavior of finite state systems, which has many applications in industry. Its main disadvantage is state space explosion problem. The basic ideas, application steps and relevant theories about model-checking are outlined by a simple example. And some approaches for dealing with the state explosion problem are introduced. At last, we compared with other verification methods, and some new achievements of software model checking are discussed briefly. |
| |
| Keywords: | model checking formal verification temporal logic |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
