Combining static analysis and case-based search space partitioning for reducing peak memory in model checking

被引：11

作者：

Zhang, WH ^{[1
]}

机构：

[1] Chinese Acad Sci, Inst Software, Comp Sci Lab, Beijing 100080, Peoples R China

来源：

JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY | 2003年 / 18卷 / 06期

关键词：

model checking; static analysis; search space partitioning; spin; protocol verification;

D O I：

10.1007/BF02945465

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Memory is one of the critical resources in model checking. This paper discusses a strategy for reducing peak memory in model checking by case-based partitioning of the search space. This strategy combines model checking for verification of different cases and static analysis or expert judgment for guaranteeing the completeness of the cases. Description of the static analysis is based on using PROMELA as the modeling language. The strategy is applicable to a subset of models including models for verification of certain aspects of protocols.

引用

页码：762 / 770

页数：9