An Innovative Heuristic to Detect Special States in Concurrent Software Systems

ABSTRACT Model checking is a formal verification technique used to verify whether a model of a given concurrent software system will meet some special states such as reachability (so‐called goal) ones, in the future. Although useful, this heuristic cannot be a suitable way in large models of given systems due to the high time of finding the similarity amount. In this paper, we present a rule‐based heuristic that uses the erase/addition of components by the rules to obtain the interdependence of rules. After acquiring these interdependences, they are employed to explore the state space efficiently. To validate the efficiency of the presented heuristic, it is applied on the concurrent software systems specified through graph transformation language, and implemented in GROOVE, an open‐source toolset for designing and model checking graph transformation systems. Experimental results show that the presented heuristic outperforms the existing algorithms in terms of running time, the number of exploration states, and the length of generated witnesses.