Model-based testing is an automated process in which executable tests are derived from behavioral models of a system. Model checking is a verification technique to reveal errors in which all reachable states of a system can be generated as state space. In the literature, different approaches suggest using model checkers for model-based testing. Model checker explores all possible system states, so utilizing the various paths in the state-space as test cases seems a promising solution. However, these approaches suffer from two main challenges. The first challenge is state space explosion, which prevents generating all reachable states by the model checker. The second one is generating redundant test cases. Recently, several methods using meta-heuristic and evolutionary approaches have been proposed to cope with these problems. Therefore, exploring a portion of state space using an optimization approach to detect the test objectives can be a proper way to manage the state space explosion and generate an optimal test suite with the least redundancy. In this paper, a method is proposed using a Bayesian optimization algorithm (BOA), and a model checker is as a bed to generate test cases for the service-oriented systems. In the proposed approach, the test suite is a set of paths on the state space starting from an initial state and leading to the state in which all the test objectives are satisfied. In this research, we have implemented BOA with three different structures in GROOVE toolset, an open-source toolset for designing and model checking graph transformation. Experimental results show that our solution generates better results in terms of coverage and speed in different case studies than the existing approaches.
