结合搜索空间划分和抽象进行LTL模型检测

被引：6

作者：

蒲飞

张文辉

机构：

[1] 中国科学院软件所计算机科学国家重点实验室

来源：

中国科学(E辑:信息科学) | 2007年 / 12期

关键词：

搜索空间划分; 求精; 抽象; LTL模型检测;

D O I：

暂无

中图分类号：

TP311.52 [];

学科分类号：

081202 ; 0835 ;

摘要：

在应用模型检测于工业系统时,状态空间爆炸仍然是一个主要的障碍.基于抽象的方法在克服状态空间爆炸方面取得了很大的成功.提出一种结合搜索空间划分和抽象的方法来降低模型检测的空间复杂度.划分依赖于每个所分划的搜索空间的表达.特别地,划分可以逐步求精以获得更好的空间消减.从数值实验看,这种搜索空间划分和抽象的结合在基于内存的需求上能提高验证的效率,同时能得到比单独使用其中一种方法更好的效果.

引用

页码：1504 / 1520

页数：17

共 9 条

[1]

Making abstract domains condensing[J] . Roberto Giacobazzi,Francesco Ranzato,Francesca Scozzari.ACM Transactions on Computational Logic (TOCL) . 2005 (1)

[2] Combining static analysis and case-based search space partitioning for reducing peak memory in model checking [J].

Zhang, WH .

JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2003, 18 (06) :762-770

[3]

Comparing Under and Over-Approximations of LTL Properties for Model Checking[J] . María del Mar Gallardo,Pedro Merino,Ernesto Pimentel.Electronic Notes in Theoretical Computer Science . 2002

[4]

Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation[J] . Lynette I. Millett,Tim Teitelbaum.International Journal on Software Tools for Technology Transfer . 2000 (4)

[5] Making abstract interpretations complete [J].

Giacobazzi, R ;

Ranzato, F ;

Scozzari, F .

JOURNAL OF THE ACM, 2000, 47 (02) :361-416

[6] Abstract interpretation of reactive systems [J].

Dams, D ;

Gerth, R ;

Grumberg, O .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1997, 19 (02) :253-291

[7] PROPERTY PRESERVING ABSTRACTIONS FOR THE VERIFICATION OF CONCURRENT SYSTEMS [J].

LOISEAUX, C ;

GRAF, S ;

SIFAKIS, J ;

BOUAJJANI, A ;

BENSALEM, S .

FORMAL METHODS IN SYSTEM DESIGN, 1995, 6 (01) :11-44

[8] MODEL CHECKING AND ABSTRACTION [J].

CLARKE, EM ;

GRUMBERG, O ;

LONG, DE .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (05) :1512-1542

[9]

Model checking modal transition systems using Kripke structures .2 Huth M. Proceedings of the12th International Conference on Verification,Model Checking and Abstract Interpretation . 2002

← 1 →