| 基于固定内存和状态管理的模型检测方法* |
| |
| 引用本文： | 吴立军,骆翔宇. 基于固定内存和状态管理的模型检测方法*[J]. 计算机应用研究, 2011, 28(6): 2164-2167. DOI: 10.3969/j.issn.1001-3695.2011.06.045 |
| |
| 作者姓名： | 吴立军 骆翔宇 |
| |
| 作者单位： | 1. 电子科技大学,计算机科学与工程学院,成都,610054
2. 清华大学,软件学院,北京,100084 |
| |
| 基金项目： | 国家自然科学基金资助项目 |
| |
| 摘 要： | 在研究固定内存和状态管理的基础上,提出了一种新的模型检测方法,使得在任何计算机上都能对任意规模的并发系统进行模型检测.
|
| 关 键 词： | 形式化方法 模型检测 状态空间爆炸 状态和内存管理 |
| 收稿时间： | 2010-12-27 |
| 修稿时间： | 2011-05-13 |
Approach of model checking based on management for fixed memory and state |
| |
| WU Li-jun,LUO Xiang-yu. Approach of model checking based on management for fixed memory and state[J]. Application Research of Computers, 2011, 28(6): 2164-2167. DOI: 10.3969/j.issn.1001-3695.2011.06.045 |
| |
| Authors: | WU Li-jun LUO Xiang-yu |
| |
| Affiliation: | (1.School of Computer Science & Engineering, University of Electronic Science & Technology of China, Chengdu 610054, China;2.School of Software, Tsinghua University, Beijing 10084, China) |
| |
| Abstract: | The model checking is one of main formal methods. Its main disadvantage is that there is the problem of state explosion and insufficient memory. Though many researchers have done a 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, presents a new approach of model checking, which makes us to finish model checking of any scale system on any computer. |
| |
| Keywords: | the formal method model checking the state explosion management of state and memory |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机应用研究》浏览原始摘要信息 |
|
点击此处可从《计算机应用研究》下载全文 |
|
