A greedy algorithm versus metaheuristic solutions to deadlock detection in Graph Transformation Systems

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

1 Introduction

The ongoing growth and presence of computer systems in our daily life and the need of mankind to speed and accuracy in doing tasks in different areas especially in big and complicated ones have caused the presence of software in these areas to be very important for solving problems. In order to prevent the development of modern software systems from getting more complicated, which normally have distributed nature and the significance of safety aspects in these systems, the use of formal approaches as effective and qualified approaches seems necessary and indispensable for assurance of quality and design accuracy. Model checking is one of the more common techniques in the confirmation of safety systems. In other words, model checking is an automatic approach for systems confirmation even before development and in the design phase.

To perform checking operations of a designed system, first we should formally describe the systems’ behavioral and structural properties. Graphs are suitable tools for explanation and modeling complicated systems structure. In this regard, Graph Transformation Systems (GTS) [1, 2] are among the visual modeling approaches and have proven to be the most useful of them.

Among GTSs, one of the obstacles in model checking is the problem of state space explosion. The state space explosion implies exponential increase in costs and applying sources with increase in model’s dimensions. In most of the cases, especially about software systems, this problem appears much because of infiniteness of state space (as a result of using recursive structures and allocating memory). A checking model system creates a graph of all possible states in order to achieve specific properties, and then traverses all the paths from one initial state to achieve the goal. If the size of the graph is very big, it will cause the problem of state space explosion in model checking system.

In order to make model checking technique practically possible, powerful techniques should be used to challenge against the problem of state space explosion. Several approaches to reduce the size of model state space have been proposed in this context such as: symbolic verification [3, 4], partial order reduction [5, 6], symmetry checking methods [7 –10] and scenario-driven model checking [11]. Model abstraction is one of the other solutions based on reducing model size. To some extent, the problem of state space explosion is improved by using given approaches, but they suffer from lack of memory in cases with extra-large state space.

Prior to this, the idea of applying intelligent approaches in model checking systems was considered less because of two major reasons: First, model checking operations are not focused on optimization in which the goal is finding the shortest or the most optimum path to the solution. Second, one major factor in designing model checking a system is their certainty, i.e. reaching the result with a degree of certainty after performing model checking operations. Whereas, the intelligent algorithms are usually considered as optimizing functions and also there isn’t any guarantee to get to the result with a high degree of certainty. However, in recent years, intelligent approaches have been taken into consideration in model checking systems, and with fewer sources in comparison with other techniques it has become possible to find existing errors in problems with extra-large state space and prevent them from happening.

Several works have been done in this context such as: applying genetic algorithms [12], ant colony algorithm [13 –15], Particle Swarm Optimization (PSO) and a hybrid algorithm using PSO and Gravitational Search Algorithm (GSA) [16].

In this paper we have tried to propose a solution based on a greedy approach using a simple intelligent algorithm in order to overcome the problem of state space explosion in GTS. A greedy algorithm is an algorithm that follows the problem solving heuristic of making the locally optimal choice at each stage with the hope of finding a global optimum. In many problems, a greedy strategy does not produce an optimal solution in general, nonetheless a greedy heuristic may yield locally optimal solutions that approximate a global optimal solution in a reasonable time [17]. Moreover, for comparison purposes, we proposed two metaheuristic algorithms, BAT and a hybrid of BAT and PSO.

The proposed algorithms concentrate on finding error states, e.g. deadlock, in state space. Finding error in modeled problems becomes possible with this proposed algorithm in considerably low time period especially in models whose state space is so wide that assurance of their correctness, considering the available facilities and the precise checking of all states of the model, is practically impossible.

The paper is organized as follows. We introduce some related works done in this context in the next section. The problem is defined in Section 3. In Section 4, applying greedy algorithm in model checking system and the implementation is discussed. Our metaheuristic algorithms proposal is described in Section 5. After that, we employ the proposed methods for several known problems in Section 6. Section 7 includes the description of the experiments performed and its comparison with the existing algorithms in this context. Finally, Section 8 defines the conclusions and future work.

2 Literature review

Normally, recommended methods in literature for overcoming the state space explosion fall into one of the following broad classifications:

2.1 Classic approach

In order to solve the problem of state space explosion in model checking systems, classic solutions such as approaches based on reducing the size of model state space [8–10 , 18–23] and the approaches based on saving memory [24 –28] have been presented. The effective approaches presented for reducing the size of model state space are: Compositional Verification, Partial Order Reduction, Symmetry Reduction. Meanwhile, there are also model abstraction approaches which reduce the size of state space by reducing the size of model. The total idea in approaches based on storing memory is using different algorithms to reduce required memory space for saving states.

2.2 Simple and metaheuristic approach

The best-first search is a simple heuristic search algorithm, which is used for protocol authentication to reach important gains over depth-first search [29]. Heuristics which choose a search pattern that favors visiting the first successor states, which are most probably to lead to an error are mentioned in [30], in the context of symbolic model checking and in [31], in the context of explicit model checking. A best-first search with Binary Decision Diagram (BDD) based on model checking, which is in the Murφ tool has been applied in [32]. Bloem et al. applied heuristics in order to reduce the bottlenecks of image calculation in symbolic model checking [33]. The authors suggested an OBDD-based version of the A* algorithm in another work [34]. The most widely known form of best-first search is called A* search [35]. Friedman et al. used a Coverage First Search correlated to structural heuristics in order to create test suites [36]. To lead a state-space search for control–dependent hardware, Ganai and Aziz also applied coverage-based techniques [37].

Heuristic approaches indicated so far are all Exhaustive Search approaches and in all of them the total state space must be searched in the worst condition. Thus, although these approaches help to find error very quickly, they suffer from the problem of state space explosion.

In recent years, some solutions have been presented by using metaheuristic, in which instead of generating the whole state space, each time only some parts of that problem are considered for search. Among the presented algorithms are: Frameworks based on reinforcement learning [38], ant colony algorithm [13 –15], genetic algorithm [39, 40] in searching and evaluating large models’ state space.

The framework based on reinforcement learning [38] has been presented to verify linear temporal properties. In this framework the goal is optimizing the use of memory through increasing the possibility of occurrence of the paths leading to properties violation. In reinforcement learning, agent is going to learn concepts through interacting with environment and getting reward and penalty.

Model checking programs are able to overcome the problem of state space explosion by applying ant colony algorithm, with inspiration from ants to find the shortest way for getting food. Having limited sources, the works done in this context have been able to find the most optimum or nearly the most optimum solution for this problem. Since these algorithms traverse the path to find the error’s root, then shorter paths are preferred to longer paths, and this fact prevent the state space explosion.

A new algorithm to search for liveness property violations in compatible systems based on ACOhg, named ACOhg-live was proposed by Francisco Chicano and Enrique Alba in [41]. A new version of Ant Colony optimization is ACOhg which was proposed in [42].

Among the works done in the context of genetic algorithm like [39, 40], is a new framework to reduce state space in concurrent reactive systems. This framework leads state space search to error states by benefitting from intelligent independent applications through using genetic algorithm. A framework is implemented in [40] by using Verisoft, which is a tool for searching systems state space. In this framework a search engine in state space of a concurrent reaction system is led to errors, such as deadlock and claim violation, through using genetic algorithm and applying intelligent approaches. Alba et al. have also introduced a framework in Java Pathfinder (JPF), a text modeling-based checking system, which is able to distinguish the deadlock [39].

Four metaheuristic algorithms which have been implemented before have been compared by the authors in [43], and also for the first time Simulated Annealing have been applied, to search the state space of such concurrent programs. The metaheuristic algorithms are Ant Colony Optimization [42], Particle Swarm Optimization [44] and two variants of Genetic Algorithm [39].

Interested readers can refer to [45] for more details about other heuristic approaches.

2.3 Simple and metaheuristic approach on GTS

Applying an approach to overcome the problem of state space explosion in verifying modeled systems is very significant, regarding the importance of graph transition systems, applied in different phases of software development like: Meta Modeling [46], Architectural Style Representation [47], Refinement [48], Refactoring [49], Model Transformation [50], Performance Analysis [51], etc.

In [52] the authors have presented abstraction technique for the exploration of GTS with infinite state spaces, called neighborhood abstraction. Also they have proposed a new method for state collapsing, based on the concept of shape subsumption. Zambon and Rensink have implemented these method in Groove [53, 54].

Isenberg et al. developed a bounded model checking (BMC) technique for GTS. In BMC technique they used first-order instead of propositional logic for encoding complex graph structures and rules. Bounded model checking [55] is a technique avoiding the state space explosion problem by focusing on bounded paths. This technique is used for finding errors, not for correctness proofs [56].

A framework has been formalized by authors in [57], for the application of heuristic search, to analyze structural properties of systems modeled by graph transition systems. In their opinion, heuristic search is aimed to reduce the analysis effort and also to find shorter solutions (i.e. shorter paths in graph transition systems). For this purpose, they use A* algorithm. This framework is implemented in HSF-SPIN, which is a heuristic model checker compatible with SPIN, the successful model checker [58].

A heuristic approach based on GA was proposed in [12] to find error states, like deadlocks in specified systems through GTS, with extra-large state space. The general idea of this approach is to develop a partial state space instead of a whole state space. For this purpose, the implemented algorithm determines which state and path should be explored in each step of space exploration. Despite the fact that genetic algorithm has proper functionality in solving optimization problems especially in large spaces, it suffers from late convergence and poor results in some cases.

In [16], the authors proposed another metaheuristic algorithm based on Particle Swarm Optimization (PSO) Algorithm. To avoid the local optima problem, they proposed a hybrid algorithm using PSO and Gravitational Search Algorithm (GSA).

In [12, 16] the authors had implemented their approach in Groove which is a tool for model checking GTS.

3 Problem definition

Our daily life dependency on computer-based applications, both hardware and software, has motivated Computer Science researchers to develop new techniques to increase our confidence on their correctness. Model checking is an automatic method for studying the properties given to a system and their verification [59]. To perform checking operations of a designed system we should describe the systems’ behavioral and structural properties formally.

Graphs play an important role in many areas of computer science and they are especially helpful in analysis and design of software applications. Graph transformation is increasingly popular as a meta-language to specify and implement visual modeling techniques, like the UML. For more information about the theoretical background and semantics of graph transformation, interested readers can refer to [1, 60].

The main challenge in model checking is dealing with the state space explosion problem. As the number of state variables in the system increases, the size of the system state space grows exponentially. This is called the state explosion problem. Much of the research in model checking over the past 30 years has involved developing techniques for dealing with this problem as we mentioned in Section 2.

We propose the solution based on a greedy approach using a simple intelligent algorithm for the finding deadlock in GTS.

Also according to the implemented approach in GA, which is based on genetic algorithm, other metaheuristic algorithms like BAT have been implemented for better comparison of the obtained results from the performance of the proposed algorithm. A combined approach has been presented in order to use the advantages of PSO and BAT algorithms simultaneously and also to overcome the defects of the mentioned algorithms. This paper is a comparison between obtained the results of metaheuristics and the proposed greedy algorithm. The structure of each algorithm’s implementation is examined next.

4 Greedy algorithms for state-space exploration

Here we explain how greedy algorithms can be used to search the state space without generating the entire state space.

A greedy algorithm is an algorithm that pursues the heuristic problem solving of making the locally optimal choice at every stage with the hope of getting a global optimum. Generally a greedy strategy does not result an optimal solution in many problems, nonetheless a greedy heuristic may produce locally optimal solutions that approximate a global optimal solution in a reasonable time. Such a strategy is guaranteed to offer optimal solutions in some cases, and in some others it may provide a compromise which produces acceptable approximations. Such algorithms can be easily invented, implemented, and most of the time they are absolutely efficient [61].

Below is a crude classification of greedy algorithm types:

Non-adaptive: fix some ordering of decisions a priori and stick with the order

Adaptive: make decisions adaptively but greedily/locally at each step

4.1 Simple combining greedy algorithm and model checking

The goal of our proposed algorithm is to intelligently generate the state space such that we can prevent state space explosion. As it has been discussed, state space is a set of states and available transitions that starts from an initial state (s₀). All the represented intelligent algorithms attempt to lead the state space generation to achieve our intended goal. The algorithm is designed such that in each state, according to the represented algorithm, the state tat has to be considered for the next traverse is chosen. In our context, a simple greedy algorithm named Best Fit Algorithm (BFA) has been proposed, inspired by correlated works done in this regard.

In order to compare the proposed algorithm with the discussed solution in [12], our concentration will be on finding an error state like deadlock in the defined state space of the problem. It has to be mentioned that deadlock is a state without outgoing transitions. BFA acts in such a way that in each level it chooses the best state among the generated outgoing states for the next traverse and it continues in this way until achieving the goal. The idea discussed in [12, 40] has been used in order to find the best state in each level among the produced states. In the represented algorithms, finding better paths for achieving the goal is based on the paths with minimum outgoing transitions. So in our proposed framework, considering suggested heuristic, rate of measurement of the produced states in each level is the state with minimum outgoing transitions. After choosing the next state by BFA, model checking system traverses the selected state and evaluates whether there is a state without outgoing transition among the produced states or not. As an example Fig. 1 shows a part of the path produced by BFA.

As can be seen, the state space production is started from s₀, assuming that s₀ has three outgoing transitions: s₁, s₂, s₃. Model checking system determines the number of each state’s outgoing transitions by producing each state from s₀. Suppose that the number of outgoing transitions of s₁, s₂ and s₃ is 4, 2, and 3, respectively. BFA algorithm, based on applied heuristic, determines that s₂ should be considered for the next traverse since s₂ includes minimum number of outgoing transitions among the available states. Now s₂ is traversed by model checking system, and as seen in the figure, s₂ has two outgoing transitions s₄, s₅. Then, it is evaluated whether there is a state without any outgoing transitions (deadlock state) among produced states from s₂. In the case of deadlock state the traverse is stopped and the error state is reported, otherwise the process of algorithm continues again. The model checking system has the ability to determine the number of outgoing transitions of a state without traversing it. For example, without traversing s₅ and s₄, it reports the number of outgoing transition of s₄, s₅ which is 4, 5, to BFA. BFA should decide, at this moment, among the states not traversed which one is the best state for next traverse. S3 is chosen in this example because among the states not traversed (s₁, s₃, s₄, s₅) it has the minimum value (the number of outgoing transitions in a state) and the algorithm continues in this way till achieving the first errorstate.

Greedy algorithms are exhaustive search and the entire state space may be traversed in the worst-case scenario. However, BFA algorithm has been able to get acceptable results in traversing state space of extra large problems in comparison with represented solutions up to now.

4.2 Using BFA in groove

Groove, a graph-based model checking tool as explained in [52, 53] has been used in order to evaluate the proposed algorithm and to compare its functionality with approaches represented for overcoming the problem of state space explosion in GTS.

In this regard, for implementing the proposed algorithm, one capability named BestFit Exploration has been embedded in the customize exploration section and in the Simulator section of Groove. This strategy has been added as a class to Groove software codes.

As discussed in the Section 4.1, in each stage, BFA determines the state that should be considered for the next traverse. The implementation method of the proposed algorithm is such that in each level of traversing, the produced states are stored in a linked list named statelist. By an added property named ‘isVisited’ in the GraphState class, predefined and available in Groove, we can determine which states have been traversed and which ones have not been chosen to traverse yet. The number of outgoing transition of each state is determined by getMatches() property and stored in an array type data structure named ‘numberOfMatch’. In each level of state space search, first the minimum value is determined in the ‘numberOfMatch’ array and it is evaluated whether its correspondent state has been traversed or not. If the state has not been traversed, it will be considered for the next traverse by Groove. Figure 2 shows the mentioned arrays based on the example elaborated in Section 4.1.

As seen in Fig. 2, the number of outgoing transitions of each state is stored in ‘numberOfMatch’ array and the algorithm gets the minimum values in this array in every time of choosing the next state for traversing, then checks the ‘isVisited’ property of the correspondent state in statelist. If it has the value of false, it is chosen for the next traverse and its value of ‘isVisited’ property becomes true and the algorithm process continues until it succeeds to find a deadlock state or in the worst condition the algorithm checks the whole search space by the described method that consequently faces the lack of memory and state space explosion. BFA’s process is shown as pseudocode in Fig. 3.

5 Metaheuristic approach for GTS

51. BAT algorithm (BA)

Yang in [62], proposed a heuristic algorithm named BAT algorithm (BA) inspired from the life of bats. BA uses echolocation feature of bats to search for food and distinguish prey from barriers.

Each bat moves in search space with velocity V_i at position X_i with loudness A_i, wavelength λ, emitted pulse rate R_i and a frequency between maximum frequency (F_max) and minimum frequency (F_min). They can adjust wavelength or frequency and the emitted pulse rate according to the proximity of bats target. In Equations 1 to 7, t is the current step and t - 1 is the previous step. In other words, t in the algorithm is the number of iterations that algorithm has done. Frequency of each bat is obtained through Equation (1) as follows: $F_{i} = F_{min} + (F_{max} - F_{min}) β$ (1) where β is a random number between 0 and 1. Then velocity and position of bats are updated respectively according to Equations (2) and (3) as mentioned below: $V_{i}^{t} = V_{i}^{t - 1} + (X_{i}^{t - 1} - X_{*}) * F_{i}$ (2) $X_{i}^{t} = X_{i}^{t - 1} + V_{i}^{t}$ (3) where X_* is the best solution among all bats. We have to change the loudness A_i and the pulse rate R_i during the algorithm iterations. As the pulse rate has increased with Equation (4) while a bat finding its prey, the loudness has decreased with Equation (5): $R_{i}^{t + 1} = R_{i}^{0} [1 - exp (- γ t)]$ (4) $A_{i}^{t + 1} = α A_{i}^{t}$ (5)

Where α and γ are invariant values and for each 0< α<1 and γ>0: $A_{i}^{t} \to 0 and R_{i}^{t} \to R_{i}^{0} when t \to \infty$ (6)

5.2 BAT algorithm based approach

A bat-based approach is proposed in this work to improve the time of deadlock detection in GTS. The ability of BAT algorithm to search the state space of the given problem is the main reason of utilizing it in the model-checking problem.

At first, position of bats was initialized randomly. Position vector contains a sequence of number in range [0, maximum number of outgoing transition-1], which is considered as a path in the state space. Velocity vector is considered as a depth search length vector of zeros. Loudness and pulse rate of the bats have been initialized depending on the problem. Each bat uses the frequency obtained from Equation (1) to update the velocity and position respectively from Equations (2) and (3).

The bats that have less emitted pulse rate than the random number between 0 and 1 select a solution among the best solutions. Then, they generate a solution close to the selected solution. In this approach, we assume that the number of states that is going to be changed is obtained as follows: $positionchange = ɛ * \bar{A^{t}}$ (7) where $\bar{A^{t}}$ is the average loudness of all bats and ɛ is a random number between 0 and 1. After the positions to be changed are determined, these positions will be changed to the same position in Gbest (best solution among all solutions). If the loudness of the certain bat is larger than a random value in range [1] and the cost of generated solution is less than the cost of Gbest then accept the new solution and update the emitted pulse rate and loudness respectively by Equations (4) and (5). The algorithm will be repeated until one of the bats reaches a deadlock.

As shown in pseudocode of BA in Fig. 4, each bat calculates its position and velocity and then uses the local search part of BA to search in the state space of the problem.

5.3 Hybrid approach based on BAT algorithm and Particle swarm optimization algorithm (BAPSO)

Although PSO is one of the most robust evolutionary algorithms, it has some flaws such as falling into trap in local optima. Recently, hybrid algorithms have been proposed to cover the disadvantage of the evolutionary algorithms [16].

In this paper, we proposed a hybrid approach by combining BAT and PSO algorithms. In this approach, the initial population was generated after defining the host graph, grammar and depth of search. P particles were considered as initial population. Each particle has some attributes (e.g. position, velocity, loudness, and pulse rate) that were initialized as mentioned in Section 5.1. After updating the global best position (Gbest) and current best position (Pbest), each particle moves in search space with PSO. Then Gbest and Pbest will be updated again and all of the particles use BAT algorithm to search in the state space of the problem. Pseudocode of BAPSO is shown in Fig. 5.

6 Evaluation

All the mentioned algorithms have been implemented in Groove to compare their results with the results of the presented algorithm in [12, 16]. The implementation of the mentioned metaheuristic algorithms utilizing the applied idea in [12] contains two phases. The first phase is a part implemented using Java in Groove environment, and the second phase, named particle manager, is implemented in.Net environment using C#. The goal of the first phase is to detect deadlock and calculate the cost of each solution and in the second phase the production of new solutions is done based on the mentioned algorithms.

The proposed greedy algorithm is implemented directly in Groove. Compared with the algorithms represented in [12, 16], in which a part of the necessary operations in the algorithm process has been considered apart from the tool, our proposed algorithm does not lead to an overhead in the algorithm running time.

You can download these models, which are modeled by Groove, via the following address: “ http://sourceforge.net/projects/projectbfa/files/BFA-BAT.rar/download”.

To detect deadlock and compare the obtained results, four famous problems, which were also experimented in [12, 16] have been used: the Dining philosophers, 8-puzzle, N-queen, Car platoon problem.

Case study

Dinning philosophers problem

The dining philosophers problem is invented by E. W. Dijkstra. Imagine that five philosophers sit around a table, which is set with 5 plates (one for each philosopher), 5 chopsticks, and a big plate of spaghetti. Each philosopher alternately thinks and eats. To eat, he needs the two chopsticks next to his plate. When finished eating, she puts the chopsticks back on the table, and continues thinking. The most serious problem of this program is that deadlock could occur. If all 5 philosophers take up their left chopstick simultaneously, the system will encounter deadlock. Pseudocode in Fig. 6 describes a philosopher process.

8-puzzle problem

The 8-puzzle is a square board with 9 positions, filled by 8 numbered tiles and one gap. At any point, a tile adjacent to the gap can be moved into the gap, creating a new gap position. In other words the gap can be swapped with an adjacent (horizontally and vertically) tile. The target in the game is to begin with an arbitrary configuration of tiles, and move them so as to get the numbered tiles arranged in ascending order either running around the perimeter of the board or ordered from left to right, with 1 in the top left-hand position. Consequently, when all the game pieces are placed in their correct place, a deadlock state is reached. An example of a 8-Puzzle problem is depicted in Fig. 7.

N-Queen problem

In chess, a queen can move as far as she pleases, horizontally, vertically, or diagonally. A chess board has 8 rows and 8 columns. The standard 8 by 8 Queen’s problem asks how to place 8 queens on an ordinary chess board so that none of them can hit any other in one move. So, deadlock in this system is the case in which 8 queens are placed on a chessboard without threatening each other. Figure 8 shows an example configuration of a 8-queens problem that queen arranged on chessboard that any queen is not at risk.

Car platoon problem

Car platooning concerns cars that drive on a highway with constant speed and constant distance from each other, to conserve energy. In this problem, one car per platoon acts as a leader of the platoon and the other cars which are called Followers, receive command messages from the leader. For this work, the cars are equipped with wireless technology. These messages are used to coordinate actions of the platoon, such as have new cars join the platoon or have the platoon change the lane. The Followers are connected to the leader through a channel. It is important that the channel must not be created between two followers. Hence, we should check either if a follower is able to send a join request to another follower or acknowledge a join request which is already sent by another leader. We consider these rules in the model as deadlock. That is, if any of the two mentioned situations happen a deadlock is occurred.

7 Results

Experiments on Groove have been done by using one processor, Core 2 Duo p8400(2.26 GHZ).

As explained in the proposed algorithms, for performing each algorithm and obtaining the results on mentioned problems (case studies), the first detected parameters in each algorithm must be initialized. Table 1 shows the initial parameters considered for performing BA and BAPSO algorithms.

To select the initial parameters in each algorithm, we investigated the proposed parameters in available literature on these algorithms which have been considered in solving the problems in different contexts. We recorded the obtained results of performing different initial parameters in each algorithm on mentioned case studies. Checking the obtained results, the considered parameters had better results on average.

The average values of 10 independent runs are shown in Table 2.

It is worth noting that all the algorithms succeeded in finding deadlock in every 10 times running.

The results in Table 2 are comparisons between six proposed algorithms, GA [12], PSO [16], PSO+GSA [16], BA, BAPSO and the proposed greedy algorithm. Each algorithm has a different performance based on the type of problem, but in general both BFA and BAPSO algorithms have an acceptable performance.

The results show that the simple BFA algorithm has been able to reduce the time for achieving the goal, considerably, in most cases. However, it is worth mentioning that the presented algorithm is based on greedy algorithms and is among exhaustive search approaches. Hence, it may create the entire state space to find a deadlock state in the worst case and consequently faces state space explosion. As seen, the results obtained from running BFA on N-Queen problem in its state space search faced the lack of memory and the greedy proposed algorithm cannot find error in it.

BAPSO has been able to get acceptable results in comparison with other metaheuristic algorithms in the cases that the state space of the problem is very big. For example, its performance result is rather impressive in 30 phil that has big and complex state space.

The significant difference between BFA and other proposed algorithms is because of directly implementing the algorithm in Groove that prevents additional overhead operations in run time.

8 Conclusion and further works

The main principle of this paper is based on overcoming the state space explosion in finding deadlock in GTS and comparing the results with the presented algorithms in this context up to now. The proposed solutions are implemented on the basis of a simple algorithm based on a greedy operation and metaheuristic algorithms.

Recently, metaheuristic algorithms are applied in a variety of problems. These algorithms can also be used in overcoming the state space explosion problem and especially in GTS.

It is important to note that in order to give priority to options within a search, or branch and bound algorithm, greedy algorithm can be applied as a selection algorithm.

However, the proposed algorithm is among exhaustive search algorithms, and hence, the model checking system may face lack of memory in searching the state space of the problem (facing state space explosion). Despite this fact, the results obtained from the proposed BFA algorithm implementation show that it has been able to get acceptable results as compared with complicated intelligent approaches implemented.

One idea for further research is that our proposed algorithm can be used to find deadlocks with different safety properties. Therefore, using these techniques, similar studies on verifying other safety properties can be performed. Also, we may be able to pay more attention and focus on choosing a better state for the next traverse using one different heuristic function. Additionally, considering different bio-inspired algorithms which are used successfully in other computing domains [63 –65] for refutation different properties can be another direction for further future works.

References

Baresi

and Heckel

, Tutorial introduction to graph transformation: A software engineering perspective, in of the First International Conference on Graph Transformation (ICGT) (2002), pp. 402–429.

Ehrig

, Engels

, Presicce

F.P.

and Rozenberg

, Graph Transformations, in ICGT, Rome, Italy, 2004.

Clarke

E.M.

, McMillan

K.L.

, Campos

S.V.A.

and Hartonas-Garmhausen

V.I.

, Symbolic model checking, Computer Aided Verification1102 (1996), 419–422.

Burch

J.R.

, Clarke

E.M.

, McMillan

K.L.

, Dill

D.L.

and Hwang

L.J.

, Symbolic model checking: States and beyond, Information and Computation98 (1992), 142–170.

Edelkamp

, Leue

and Lafuente

A.L.

, Directed explicit-state model checking in the validation of communication protocols, International Journal on Software Tools for Technology (STTT)5 (2004), 247–267.

Bošnački

, Leue

and Lafuente

A.L

, Partial-order reduction for general state exploring algorithms, International Journal on Software Tools for Technology Transfer (STTT)11 (2009), 39–51.

Lafuente

A.L.

, Symmetry reduction and heuristic search for error detection in model checking, Workshop on Model Checking and Artificial Intelligence, 2003.

Emerson

E.A.

and Sistla

A.P.

, Symmetry and model checking, Formal Methods in System Design - Special Issue on Symmetry in Automatic Verification9 (1996), 105–131.

Clarke

E.M.

, Enders

, Filkorn

and Jha

, Exploiting symmetry in temporal logic model checking, Formal Methods in System Design - Special Issue on Symmetry in Automatic Verification9 (1996), 77–104.

10.

Gyuris

and Sistla

A.P.

, On-the-fly model checking under fairness that exploits symmetry, Formal Methods in System Design15 (1999), 217–238.

11.

Rafe

and Scenario-driven analysis of systems specified through graph transformations, Visual Languages and Computing, (online first January2013).

12.

Yousefian

, Rafe

and Rahmani

, A heuristic solution for model checking graph transformation systems, Applied Soft Computing24 (2014), 169–180.

13.

Lucio Mauro Duarte

L.F.

, Wagner

F.R

and Heimfarth

, Model checking the ant colony optimisation, Computer Science329 (2010), 221–232.

14.

Francisco

E.A.

, Chicano, Ant Colony Optimization in Model Checking, in of the 11th International Conference on Computer Aided Systems Theory, Springer-Verlag, Berlin, Heidelberg, 2007, pp. 523–530.

15.

Francesca

, Santone

, Vaglini

and Villani

M.L.

, Ant Colony Optimization for Deadlock Detection in Concurrent Systems, in: Of the 2011 IEEE 35th Annual Computer Software and Applications Conference IEEE Computer Society Washington, DC, USA2011, pp. 108–117.

16.

Rafe

, Moradi

, Yousefian

and Nikanjam

, A meta-heuristic solution for automated refutation of complex software systems specified through graph transformations, Applied Soft Computing33 (2015), 136–149.

17.

Chang

S.K.

, Data Structures and Algorithms: World Scientific, 2003.

18.

Valmari

, Error detection by reduced reachability graph generation, in: Application and Theory of Petri Nets - APN, Venice, Italy, 1988.

19.

Valmari

, Heuristics for Lazy State Generation Speeds up Analysis of Concurrent Systems, in: Finnish Artificial Intelligence Symposium STeP-88, Helsinki, (1988), pp. 640–650.

20.

Godefroid

and Wolper

, Using partial orders for the efficient verification of deadlock freedom and safety properties, Formal Methods in System Design - Special Issue on Computer-Aided Verification: Special Methods II2 (1991), 149–164.

21.

Godefroid

, Using Partial Orders to Improve Automatic Verification Methods, UK, pp, in: Of the 2nd International Workshop on Computer Aided Verification Springer-Verlag London (1991), 176–185.

22.

de Roever

W.P.

, The Need for Compositional Proof Systems: A Survey, in: COMPOS’97 Revised Lectures from the International Symposium on Compositionality: The Significant Difference Springer-Verlag London1998, pp. UK, 1–22.

23.

Peng

and Tahar

, A Survey on Compositional Verification, Available at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.29.4911&rep=rep1&type=pdf, 1998.

24.

Courcoubetis

, Vardi

, Wolper

and Yannakakis

, Memory efficient algorithms for the verification of temporal properties, Formal Methods in System Design - Special Issue on Computer-Aided Verification1 (1992), 275–288.

25.

Stern

and Dill

D.L.

, Improved Probabilistic Verification by Hash Compaction, in: Of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods Springer-Verlag London, UK, 1995, pp. 206–224.

26.

Stern

and Dill

D.L.

, A New Scheme for Memory-Efficient Probabilistic Verification, On formal descrition techniques IX/protocol specification, testing and verification XVI on Formal description techniques IX: Theory, application and tools: Theory, application and tools, Chapman & Hall, Ltd, London, UK, 1996, pp. 333–348

27.

Wolper

and Leroy

, Reliable hashing without collision detection, pp, in: Computer Aided Verification 5th International Conference (1993), 59–70.

28.

Sivaraj

and Gopalakrishnan

, Random walk based heuristic algorithms for distributed memory model checking, Electronic Notes in Theoretical Computer Science (ENTCS)89 (2003), 51–67.

29.

Lin

F.J.

, Chu

P.M.

and Liu

M.T.

, Protocol verification using reachability analysis: The state space explosion problem and relief strategies, in: ACM Workshop on Frontiers in Computer Communications Technology (1987), pp. 126–135.

30.

Yang

C.H.

, Prioritized Model Checking in, Stanford University, 1998.

31.

Edelkamp

, Lafuente

A.L.

and Leue

, Directed explicit model checking with HSF-SPIN, in: SPIN Workshop, 2001, pp. 57–79.

32.

Yang

C.H.

and Dill

D.L.

, Validation with guided search of the state space, in: DAC ’98 Proceedings of the 35th annual Design Automation Conference, 1998, pp. 599–604.

33.

Bloem

, Ravi

and Somenzi

, Symbolic Guided Search for CTL Model Checking, in: Design Automation2000, pp. 29–34.

34.

Edelkamp

and Reffel

, OBDDs in Heuristic Search, Springer, Advances in Artificial Intelligence, 1998, pp. 81–92.

35.

Russell

S.J.

and Norvig

, Artificial Intelligence: A Modern Approach, third edition, 2009.

36.

Friedman

, Hartman

, Nagin

and Shiran

, Projected state machine coverage for software testing, in: ACM SIGSOFT International Symposium on Software Testing and Analysis2002, pp. 134–143.

37.

Ganai

M.K.

and Aziz

, Efficient Coverage Directed State Space Search, In International Workshop on Logic Synthesis (1998).

38.

Behjati

, Sirjani

and Ahmadabadi

M.N.

, Bounded rational search for on-the-fly model checking of LTL properties, in: Of the Third IPM International Conference on Fundamentals of Software Engineering Springer-Verlag Berlin, Heidelberg, 2010, pp. 292–307.

39.

Alba

, Chicano

, Ferreira

and Pulido

J.G.

, Finding deadlocks in large concurrent java programs using genetic algorithms, in: Of the 10th Annual Conference on Genetic and Evolutionary Computation, New York, NY, USA, 2008, pp. 1735–1742.

40.

Godefroid

, Khurshid

, Exploring very large state spaces using genetic algorithms, on Software Tools for Technology Transfer (STTT) - Special Section on Tools and Algorithms for the Construction and Analysis of Systems6 (2004), 117–127.

41.

Alba

and Chicano

, Searching for Liveness Property Violations in Concurrent Systems with ACO, Presented at the Proceedings of the 10th Annual Conference on Genetic and Evolutionary Computation, Atlanta, GA, USA, 2008, pp. 1727–1734.

42.

Alba

and Chicano

, Finding safety errors with ACO, Presented at the Proceedings of the 9th Annual Conference on Genetic and Evolutionary Computation, London, England, 2007, pp. 1066–1073.

43.

Chicano

, Ferreira

and Alba

, Comparing Metaheuristic Algorithms for Error Detection in Java Programs, in Third International Symposium, SSBSE2011, pp. 82–96.

44.

Ferreira

, Chicano

, Alba

, Chicano

and Alba

, Detecting protocol errors using particle swarm optimization with java pathfinder, Presented at the High Performance Computing & Simulation Conference2008, pp. 319–325.

45.

Groce

and Visser

, Heuristics for model checking java programs, International Journal on Software Tools for Technology Transfer6 (2004), 260–276.

46.

Engels

, Hausmann

J.H.

, Heckel

and Sauer

, Dynamic Meta Modeling: A Graphical Approach to the Operational Semantics of Behavioral Diagrams in UML, in: The 3rd International Conference on The Unified Modeling Language: Advancing the Standard (UML’00), Springer, 2000, pp. 323–337.

47.

Mahdian

, Rafe

, Rafeh

and Miralvand

M.R.Z.

, Considering Faults in Service-Oriented Architecture: A Graph Transformation-Based Approach, in: International Conference on Computer Technology and Development, 2009.

48.

Heckel

and Thöne

, Behavioral refinement of graph transformation-based models, Electronic Notes in Theoretical Computer Science (ENTCS)127 (2005), 101–111.

49.

Mens

, On the Use of Graph Transformations for Model Refactoring, Springer, in: Generative and Transformational Techniques in Software Engineering (GTTSE’05)2005, pp. 219–257.

50.

Taentzer

, Ehrig

, Guerra

, de Lara

, Lengyel

, Levendovszky

, et al., Model Transformation by Graph Transformation: A Comparative Study, in: Workshop Model Transformation in Practice, Software and System modelings (Sosym), 2005.

51.

Naddaf

M.R.

and Rafe

, Performance modeling and analysis of software architectures specified through graph transformations, Computing and Informatics32 (2013), 797–826.

52.

Zambon

and Rensink

, Graph Subsumption in Abstract State Space Exploration, in GRAPHITE, 2012, pp. 35–49.

53.

Kastenberg

and Rensink

, Model Checking Dynamic States in GROOVE, in: Of the 13th International Conference on Model Checking Software Springer-Verlag Berlin, Heidelberg, 2006, pp. 299–305.

54.

Rensink

, Boneva

, Kastenberg

and Staijen

, User Manual for the GROOVE Tool Set, Available at http://groove.cs.utwente.nl/wp-content/uploads/usermanual1.pdf, 2010.

55.

Rafe

and Rahmani

A.T.

, Towards automated software model checking using graph transformation systems and Bogor, Journal of Zhejiang University SCIENCE A10(8), 1093–1105.

56.

Isenberg

, Steenken

and Wehrheim

, Bounded model checking of graph transformation systems via SMT solving, Formal Techniques for Distributed Systems7892 (2013), 178–192.

57.

Edelkamp

, Jabbar

and Lafuente

A.L.

, Heuristic search for the analysis of graph transition systems, in: Graph Transformation (ICGT), 2006.

58.

Holzmann

G.J.

, The model checker SPIN, IEEE Transactions on Software Engineering23 (1997), 279–295.

59.

Baier

and Katoen

J.P.

, Principles of Model Checking, 2008.

60.

Ehrig

, Engels

, Kreowski

H.J.

and Rozenberg

, Languages and Tools, Handbook of Graph Grammars and Computing by Graph Transformation: Applications, 1999.

61.

Cormen

T.H.

, Leiserson

C.E.

, Rivest

R.L.

and Stein

, Introduction to Algorithms:, MIT Press, 2011.

62.

Yang

X.-S.

, A new metaheuristic bat-inspired algorithm, Nature Inspired Cooperative Strategies for Optimization (NICSO 2010)284, 65–74.

63.

Jamali

, Jahanbakhsh

, BA-TORA: A Multipath Routing Protocol for MANETs by Inspiration from Bee and Ant Colonies, Electrical Review, 2011, pp. 183–187.

64.

Jamali

and Shaker

, PSO-SFDD: Defense against SYN flooding DoS attacks by employing PSO algorithm, Computers & Mathematics with Applications63(1) (2012), 214–221. Elsevier.

65.

Jamali

and Shaker

, Defense against SYN flooding attacks: A particle swarm optimization approach, Computers & Electrical Engineering40(6) (2014), 2013–2025. Elsevier.