A heuristic solution for model checking graph transformation systems

被引:32
作者
Yousefian, Rosse [1 ]
Rafe, Vahid [1 ]
Rahmani, Mohsen [1 ]
机构
[1] Arak Univ, Fac Engn, Dept Comp Engn, Arak 3815688349, Iran
关键词
State space explosion; Model checking; Graph transformation systems; Genetic algorithm; VERIFICATION; SYMMETRY;
D O I
10.1016/j.asoc.2014.06.055
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
One of the commonly used techniques to verify software and hardware systems which have been specified through graph transformation system (GTS), especially safety critical ones, is model checking. However, the model checking of large and complex systems suffers from the state space explosion problem. Since genetic algorithm (GA) is a heuristic technique which can be used to search the state space intelligently instead of using exhaustive methods, in this paper, we propose a heuristic approach based on GA to find error states, such as deadlocks, in systems specified through GTS with extra large state space. To do so, in each step of space exploration our algorithm determines which state and path should be explored. The proposed approach is implemented in GROOVE, a tool for model checking graph transformation systems. The experimental results show that our approach outperforms significantly in comparison with existing techniques in discovering error states of models with large state space. (C) 2014 Elsevier B.V. All rights reserved.
引用
收藏
页码:169 / 180
页数:12
相关论文
共 69 条
[1]  
Alba E., 2008, P 10 ANN C GEN EV CO, P1735
[2]  
[Anonymous], WORKSH MOD CHECK ART
[3]  
[Anonymous], 2003, ELECTRON NOTES THEOR
[4]  
[Anonymous], 2004, Wiley InterScience electronic collection.
[5]  
[Anonymous], EATCS MONOGRAPHS TCS
[6]  
[Anonymous], 1999, INTRO GENETIC ALGORI
[7]  
Backes P., 2010, TRANSFORMATION TOOL, p[WP10, 107]
[8]  
Baldan P., 2004, INT C CONC THEOR CON
[9]  
Baresi L, 2002, LECT NOTES COMPUT SC, V2505, P402
[10]  
BARESI L, 2003, 9 EUR SOFTW ENG C HE, V28, P68