MS-ACO: a multi-stage ant colony optimization to refute complex software systems specified through graph transformation

Model checking is one of the successful techniques in automated verification of software and hardware systems. However, employing this technique for verification of properties such as the safety and liveness requires that all possible states of a system are generated and then the given property is checked. In large and complex systems, generating all states causes the state space explosion problem. Hence, it is possible to refute such properties by searching the state space to find a state in which the given property is violated. Of course, it is possible that detecting such states in complex systems leads to the exhaustive exploration of the state space. Recent researches confirm that using meta-heuristic and evolutionary approaches to intelligently explore a portion of the state space can be a promising idea. Hence, in this paper, we propose an approach based on ant colony optimization algorithm for refuting the safety and liveness properties and also analyzing reachability ones in systems specified formally through graph transformation system. Refutation of liveness and analyzing reachability properties in systems modeled by graph transformations are the prominent advantages of this approach in comparison with the previous approaches. The proposed approach is implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. Experimental results show that our proposed approach is faster and it generates shorter counterexamples in comparison with others.