An efficient approach to state space management in model checking of complex software systems using machine learning techniques

摘要

Since complexity of computer systems is growing increasingly, assuring flawless operation of these systems has become more difficult. Therefore, it is important that these systems whether software or hardware are executed as expected. Consequently, verifying system before implementation at model level is necessary. Model checking is a formal technique for validating the system automatically which decides whether the finite state system satisfies temporal property by scanning the whole state space or not. One of the most important problems in model checking is state space explosion of models which results in memory shortage in generation of all states. Therefore, this paper presents a method which employs machine learning techniques without exploring the whole state space to predict temporal properties of trajectories in systems based on graph transmission system. the proposed method is implemented in Groove; results indicate desirable accuracy and speed of this method compared to other methods.