Performance and Reliability Analysis of Web Service Composition Using Probabilistic Model Checking
Khadidja Salah Mansour, Youcef Hammal · International Journal of Web Engineering and Technology · 2025
Design and implementation of composite software systems by integrating loosely coupled individual web services are still an important issue within the SOA topic even though they still face significant complexities related to compatibility challenges which arise from their independent development processes. Our key aim is hence to provide an in-depth formal analysis of compatibility issues encountered in composite service and propose a comprehensive methodology to effectively address these challenges. We propose a formalisation and verification approach to tackle the crucial problem of services integration that always hinders reliable composition of distributed services. This paper focuses on ensuring functional and non-functional correctness of composite services described using WS-BPEL. These descriptions are first translated into communicating automata and then checked against intended specifications defined by WS-CDL. In order to enable probabilistic model checking of the composite service using the PRISM tool, the external choreography properties are formalised into formulae of PCTL.