Affiliations: [a]
Sama Technical and Vocatinal Training College, Islamic Azad University, Khomeinishahr Branch, Isfahan, Iran
| [b]
Department of Computer Engineering, Faculty of Engineering Arak University, Arak 38156-8-8349, Iran
Correspondence:
[*]
Corresponding author. Rosa Yousefian, Sama Technical and Vocatinal Training College, Islamic Azad University,
Khomeinishahr Branch, Isfahan, Iran. E-mail: Rosa8a81@yahoo.com.
Abstract: Nowadays, using model checking techniques is one of the best solutions for software (and hardware) verification. The problem while using model checking techniques is state space explosion in which all the available memory is consumed by the model checker to generate all the reachable states. Among different approaches to cope with the state space explosion problem, using heuristic and meta-heuristic algorithms seems a proper solution. Although in all of these approaches it is not possible to solve the problem totally, however, it is possible to use them as refutation techniques. In the meta-heuristic techniques it is tried to generate only a portion of the state space with the highest probability to reach a faulty state. In this paper, we propose two new algorithms to deadlock detection in complex software systems specified through graph transformation systems. The first approach is a hybrid algorithm using PSO and BAT (BAPSO) and the second one is a greedy algorithm to find deadlocks. The experimental results show that the hybrid approach (BAPSO) is more accurate than PSO, BAT and other existing approaches like Genetic Algorithm (GA). In addition, in most of the case studies, the proposed greedy algorithm can compete with the meta-heuristic algorithms in terms of speed and accuracy.
Keywords: State space explosion, model checking, Graph Transformation Systems, genetic algorithm, BAT algorithm, Particle swarm optimization algorithm, greedy algorithm
