An Efficient Bounded Model Checking Approach for Web Service Composition

With the development of service-oriented architecture, Web service composition has become more important for mitigating potential security vulnerabilities. When the scale of services increases, it will lead to the problem of state explosion. Symbolic model checking is a common method used to alleviate the problem of state-space explosion. However, for a large Web service composition system, the number of services is large, and the corresponding state space may exceed the magnitude of the symbolic model checking that can verify it. As it alleviates the state-space explosion problem, bounded model checking was utilized in the present study to verify the properties of the service composition system. Bounded model checking searches for bounded counterexamples in a limited local space and reduces the state space. This study verifies the composition of semantic Web services described by OWL-S and proposes a timed service model (TSM) to formally model the service composition system. Furthermore, the auto-mapping relationship between the OWL-S service description and the model is established. For more efficient verification, this study uses SMT-based (SMT: satisfiability modulo theory) encoding in the TSM. Finally, a public emergency service composition system was built to verify the proposed model and the efficiency of the proposed algorithm.