|
چکیده
|
While developing concurrent systems, one of the important properties to be checked is deadlock free- dom. Model checking is an accurate technique to detect errors, such as deadlocks. However, the problem of model checking in complex software systems is state space explosion in which all reachable states cannot be generated due to exponential memory usage. When a state space is too large to be explored exhaustively, using meta-heuristic and evolutionary approaches seems a proper solution to address this problem. Recently, a few methods using genetic algorithm, particle swarm optimization and similar ap- proaches have been proposed to handle this problem. Even though the results of recent approaches are promising, the accuracy and convergence speed may still be a problem. In this paper, a novel method is proposed using Bayesian Optimization Algorithm (BOA) to detect deadlocks in systems specified for- mally through graph transformations. BOA is an Estimation of Distribution Algorithm in which a Bayesian network (as a probabilistic model) is learned from the population and then sampled to generate new so- lutions. Three different structures are considered for the Bayesian network to investigate deadlocks in the benchmark problems. To evaluate the efficiency of the proposed approach, it is implemented in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental re- sults show that the proposed approach is faster and more accurate than existing algorithms in discovering deadlock states in the most of case studies with large state spaces.
|