Article Preview
Top1. Introduction
The present information systems in companies are complex structures involving competition, communication and coordination. They are based on applications that exchange data and participate in business processes which are built around Web services that perform different types of tasks. When Web services come from multiple agencies (in the case of inter-company collaborations), it quickly falls into the problem of data heterogeneity and their formats. Different standards and languages have been proposed in the literature to model the composition of Web services, including WSCI (Assaf, Sid, Scott, & Wolfgang, 2002), BPML (Arkin A., 2002), WSFL (Leymann, 2001), XLANG (Thatte, 2001), WSCI (Arkin, Askary, Fordin, Jekeli, & Kawaguchi, 2002) and WS-BPEL (Jordan, et al., 2007). Unfortunately, these languages are textual and ignore the specification stage. In addition, the formal analysis of the proposed language is not possible due to the lack of formal semantics of these languages. It is therefore necessary to develop methods of specification, and formal verification for controlling the end-to-end development process.
One of the emerging languages for specifying business process behavior based on Web services is Web Services Business Process Execution Language (abbreviated to WS-BPEL or BPEL) that has become the standard for the description of Web services compositions. It has been officially specified in (Jordan, et al., 2007). This specification is much more detailed and more precise compared to the predecessor specification (Andrews, et al., 2003), but as we have said previously the textual specification of BPEL is not adapted for formal methods. To formally analyze properties of BPEL processes, it is necessary to understand the semantics of the original specification and resolve the ambiguities and inconsistencies of this language. In the literature, many proposals have emerged to analyze BPEL Web services. However, most of which are grounded on BPEL untimed behavior.
In this work we are interested in formal verification and analysis of the Web services composition. We give a transformation approach enabling us to model the behavior of BPEL Web services by a real-time specification language and to describe formally the behavior of each operator of the Web services composition language. We have not only to verify the behaviors generated by the interactions of a set of BPEL Web services, such as safety, liveness and deadlock freeness in the composition execution (qualitative requirements), but also to analyze the timed properties of BPEL Web services compositions, such as actions incompatibility, auto-concurrency level and specification of the concurrency degree (Guellati, Kitouni, Matmat, & Saidouni, 2014) (quantitative properties). We define a mapping from executable Web services written in BPEL to an abstract specification written in the real-time language D-LOTOS (Saïdouni & Courtiat, 2003). This translation includes also compensation handler, event handler, fault handler, and takes into account the timing constraints and the duration of interactions between Web services.
In our knowledge, this work is the first one that consider both timed constraints and the durations of interactions between web services. In addition, the use of a real-time language which is based on true-concurrency semantics (Saidouni, Belala, & Bouneb, 2008) allows the specification of parallel execution of activities which elapse in time. This aspect constitutes the novelty of our method in comparison of existing ones.