A Formal Approach for the Validation of Web Service Orchestrations

Introduction

A service Oriented Architecture (SOA for short) (Papazoglou, 2003) is a software architecture. It focuses on delivering functionality through loosely coupled services that can be reused across the enterprise in defined sequences to fulfill business processes. The services in this architecture are independent and operate without any context from other processes or services within the organization. Web services are considered as the best standard based way to realize SOA. They are a building block in the sense that they can be composed to form higher level services or applications to achieve business goals. They are called composite when their executions involve interactions with other web services so as to use their features (Curbera et al., 2003). The web service composition determines what services need to be invoked, in what order and how to handle exceptional conditions. In orchestration, the involved web services are under the control of a single endpoint central process (orchestrator). This process coordinates the execution of various actions on the web services involved in the composition.

However, some conflicts can be generated in the web service orchestration as soon as they interact together such as deadlock and incoherent messages exchange. To overcome these problems, it is necessary to use formal methods to check the web service orchestration. Indeed, after each expert has defined his composition process, he has to ensure the system evolution by the verification of some standard properties such as liveness, safety, deadlock and so on (HadjKacem et al., 2012). These properties are considered generic since they are checked on the invoked services regardless of the activities which compose them. We deem that another type of properties has to be checked. These properties deal with activities in an orchestration process. They are considered, in this paper, as specific properties (HadjKacem et al., 2012a). For instance, we can consider the online payment process case, the two encryption activities “StrongEncrypt” and “WeakEncrypt” are both fulfill the confidentiality, but when combined their effect would be a twice encrypted message, which generates serious errors in decryption. These two activities are related to each other with a choice interdependency and they should not be chosen for the same process. Also, during the application control access, the requirement property has to be maintained between authenticity and authorization activities. An authenticity activity must precede the authorization to decide if the user has the right to access. These two activities are related to each other with a prerequisite interdependency.

These properties and others, presented as non-functional concerns in (Sanen et al., 2007) and (Schmeling et al., 2010), will be considered here to verify a web service orchestration. In this context, several solutions were proposed in order to verify a web service orchestration (Abouzaid et al., 2009; Kovacs et al., 2008; Kazhamiakin et al., 2006; Dekdouk et al., 2005). These solutions are only based on the generic properties verification. To our knowledge, no solution has been proposed taking into account the specific properties. In this paper, we overcome these difficulties by proposing a formal approach for the validation of web service orchestrations since the verification process cannot be directly achieved in the composition process. Here, we adopt WS-BPEL 2.0 (Barreto et al. 2007) as the language to describe the web service orchestration and we propose using SPIN model-checker (Holzmann, 2003) for the verification process. SPIN is a generic verification tool that supports both the design and the verification of the asynchronous process systems.

Our approach takes into account both generic and specific properties:

• •

  Generic Properties: They allow us to gather all standard properties having the same active behaviour and can be checked in any involved service in the orchestration.

• •

  Specific Properties: They are related to interdependence relations between activities in a WS-BPEL process. We classify these properties into three subclasses: exclusion, inclusion and prerequisite relations.