Affordable Access

Publisher Website

A heuristic solution for model checking graph transformation systems

Applied Soft Computing
DOI: 10.1016/j.asoc.2014.06.055
  • State Space Explosion
  • Model Checking
  • Graph Transformation Systems
  • Genetic Algorithm
  • Astronomy
  • Computer Science
  • Mathematics


Abstract 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.

There are no comments yet on this publication. Be the first to share your thoughts.