一种自动的形式化验证技术——模型检测  

Model-Checking-An Automatic Formal Verification Technique

作　　者：化志章[1] 揭安全[1] 薛锦云[1] 

机构地区：[1]江西省高性能计算技术重点实验室

出　　处：《微计算机信息》2007年第33期254-256,222,共4页Control & Automation

基　　金：国家重大基础研究前期研究专项(973计划)(2003CCA02800);国家自然科学基金项目(60273092);江西省教育厅科技项目(2005-90)

摘　　要：模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单介绍了软件模型检测的新进展.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.

关 键 词：模型检测 形式验证 时态逻辑 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]