Formal Reliability Models for Web Services

In Web services (WS), software applications are dynamically built by assembling over a network existing, loosely coupled, distributed, and heterogeneous services. Reliability is one of the most important quality dimensions for Web services, since predicting their reliability is fundamental to appropriately drive the selection and the assembly of services. This chapter presents two approaches to predict the reliability of a Web service architecture. The first one is based on the Business Process Execution Language (BPEL), the de facto standard executable language for specifying actions within business processes with Web services. The second one is based on the SCA-ASM, a lightweight formal language for modeling service-oriented applications, which is based on the OASIS (Organization for the Advancement of Structured Information Standards) standard Service Component Architecture for heterogeneous service assembly and on the formal method abstract state machines (ASMs) for modeling service behavior, interactions, and orchestration in an abstract but executable way. Through a set of experimental results, we show how the two models work on a smartphone mobile application example, and we discuss the effectiveness of the SCA-ASM approach in comparison with the BPEL-based approach.