版权所有:内蒙古大学图书馆 技术提供:维普资讯• 智图
内蒙古自治区呼和浩特市赛罕区大学西街235号 邮编: 010021
作者机构:Islamic Azad Univ Khomeinishahr Branch Sama Tech & Vocatinal Training Coll Esfahan Iran Arak Univ Dept Comp Engn Fac Engn Arak *** Iran
出 版 物:《JOURNAL OF INTELLIGENT & FUZZY SYSTEMS》 (智能与模糊系统杂志)
年 卷 期:2016年第31卷第1期
页 面:137-149页
核心收录:
学科分类:12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 08[工学] 0812[工学-计算机科学与技术(可授工学、理学学位)]
主 题:State space explosion model checking Graph Transformation Systems genetic algorithm BAT algorithm Particle swarm optimization algorithm greedy algorithm
摘 要: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.