a hybrid meta-heuristic approach to cope with state space explosion in model checking technique for deadlock freeness

Model checking is an automatic technique for software verification through which all the reachable states are generated from an initial state in order to find the errors and desirable patterns. in the model checking approach, the behavior and structure of the system should be modeled. the graph transformation system is a graphical formal modeling language used to specify and model the system. however, modeling large systems with the graph transformation system suffers from the state space explosion problem, which usually requires huge amounts of computational resources.in this paper, we propose a hybrid meta-heuristic approach in order to deal with this searching problem in the graph transformation system because meta-heuristic algorithms are efficient solutions to traverse the graph of large systems. using the artificial bee colony and simulated annealing, our approach replaces a full state space generation, only by producing part of it checking the safety, and finding the errors (e.g. deadlock). the experimental results obtained show that the proposed approach is more efficient and accurate compared with other approaches.