|
چکیده
|
The model checking technique is a formal and effectual way in verification of software systems. By the 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 the 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 existing 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 opensource tool for designing and studying the model of graph transformation systems. The results show that, in addition to increasing the intelligence of the model checking process, the suggested method requires less initial parameter adjustment. The proposed approach is implemented on several well-known problems. According to the experimental results, the proposed method performs better than the earlier ones in terms of average run time, the number of explored modes and the accuracy
|