| 模型检测新技术研究 |
| |
| 引用本文： | 戎玫,张广泉.模型检测新技术研究[J].计算机科学,2003,30(5):102-104. |
| |
| 作者姓名： | 戎玫 张广泉 |
| |
| 作者单位： | 1. 暨南大学中旅学院,深圳,518053
2. 苏州大学计算机科学与技术学院,苏州,215006;中国科学院软件所计算机科学重点实验室,北京,100080 |
| |
| 基金项目： | 国家863高科技项目(2001AA113200)，重庆市应用基础研究项目，中国科学院计算机科学重点实验室资助 |
| |
| 摘 要： | 1 引言软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一,尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety-critical)领域更是如此。这类系统要求绝对安全可靠,不容半点疏漏,否则将导致灾难性后果。如1996年6月4日,欧洲航天局阿丽亚娜(Ariane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜,如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。
|
| 关 键 词： | 软件开发 软件可靠性 形式化方法原则 软件系统 演绎推理 模型检测 |
New Approaches for Model Checking |
| |
| RONG Mei ZHANG Guang-Quan.New Approaches for Model Checking[J].Computer Science,2003,30(5):102-104. |
| |
| Authors: | RONG Mei ZHANG Guang-Quan |
| |
| Abstract: | Model checking is an algorithmic verification technique that checks automatically whether a given finite state concurrent system satisfies its temporal specification. The main disadvantage of model checking is state space explosion problem. In this paper, several important approaches have been proposed for dealing with the state explosion problem. Such approaches are symbolic, abstraction, partial.order reduction, compositional reasoning, etc. Then,a number of way are proposed for verifying real.time and hybrid systems using model checking. At last, several approaches combining model checking and other verification techniques or mathematical methods are considered. |
| |
| Keywords: | Model checking State explosion Symbolic model checking Abstraction Partial-order reduction Compositional reasoning Real-time system Hybrid system |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
