A heuristic solution for model checking graph transformation systems

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.