Formal modeling and verification of cloud‐based web service composition
Syed Asad Raza Kazmi, Awais Qasim, Adnan Khalid, Ruttaba Assad, Muhammad Shahbaz · Concurrency and Computation Practice and Experience · 2019
Summary Web service composition is a key technology to resolve cross‐organizational business process integration, and it faces many constraints and requirements as unexpected bugs can cause shutdown of the software. A high degree of reliability is expected from such systems, and formal modeling of web service composition is an active area of research. In this work, we propose a new approach for the formal modeling of diverse web service composition. Our approach verifies the terminate property on all possible runs of the system to ensure deadlock‐free workings. For a verification of the properties of interest, we use the NuSMV model checker and specify the properties in CTL*. The approach can be used to verify the soundness property of diverse web service composition to ensure live and deadlock‐free web services.