Checking Reachability Property in Complex Concurrent Software Systems with a Knowledge Discovery Approach

The model checking technique is a formal and effectual way in verification of software systems. By generation and investigation of all model states, it analyses the software systems. The main issue in the model checking of the complicated systems having wide or infinite state space is the lack of memory in generation of all states which is referred to as "state space explosion". The Random Forest algorithm which is capable of knowledge discovery faces the above-cited problem by selecting a few promising paths. In our suggested method, first a small model of the system is developed by the formal language of graph transformation system (GTS). A training data set is created from the small state space. The generated training data set is made available to the Random Forest algorithm to detect and discover the logical relationships existent in it. Then, the knowledge acquired in this way is used in the smart and incomplete exploration of the large state space. The proposed approach is run in GROOVE which is an open source tool for designing and studying the model of graph transformation systems. The results indicate that the suggested method in accordance with the two criteria (average running time and the number of explored states) performs better compared with the other approaches.