|
|||||
|
|
| 基于动态内存和状态管理的模型检测新方法 | |
| 引用本文： | 吴立军,骆翔宇,陈清亮.基于动态内存和状态管理的模型检测新方法[J].计算机科学,2011,38(11):191-195. |
| 作者姓名： | 吴立军 骆翔宇 陈清亮 |
| 作者单位： | 1. 电子科技大学计算机科学与工程学院 成都610054 2. 清华大学软件学院 北京100084 3. 暨南大学计算机科学学院 广州410074 |
| 基金项目： | 国家自然科学基金项目(61073033,60763004)资助 |
| 摘 要： | 模型检测是并发系统验证的主要形式化方法之一,但其存在因状态空间爆炸而导致内存不够的问题,这也是大规模并发系统验证的瓶颈.很多研究人员尽管做了很多相关研究,但仍然没有很好地解决这个问题.在研究动态内存和状态管理的基础上,提出了一种新的模型检测方法,避免了因为内存不足而无法模型检测的问题. |
| 关 键 词： | 形式化方法 模型检测 状态空间爆炸 状态和内存管理 |
New Approach of Model Checking Based on Management for Dynamic Memory and State |
|
| WU Li-jun,LUO Xiang-yu,CHEN Qing-liang.New Approach of Model Checking Based on Management for Dynamic Memory and State[J].Computer Science,2011,38(11):191-195. | |
| Authors: | WU Li-jun LUO Xiang-yu CHEN Qing-liang |
| Affiliation: | WU Li-jun1 LUO Xiang-yu2 CHEN Qing-liang3(School of Computer Science,University of Electronic Science and Technology,Chengdu 610054,China)1(School of Software,Tsinghua University,Beijing 100084,China)2(Department of Computer Science,Jinan University,Guangzhou 410074,China)3 |
| Abstract: | Abstract The model checking is one of main formalization methods. However there is the problem about state explosion and insufficient memory, which is bottleneck of verification of large scale systems. hhough many researchers have done amount of work, the problem has not been settled well yet. The paper, based on the investigation of the management for fixed memory and state, presented a new approach of model checking, which avoids the problem that model checking can not proceed because of insufficient memory. |
| Keywords: | Formal method Model checking State explosion Management of state and memory |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |
| 点击此处可从《计算机科学》浏览原始摘要信息 | |
| 点击此处可从《计算机科学》下载全文 | |