Approach
In the realm of SOA paradigm, choreography analysis helps to know if a set of services can lead or not to a correct interaction. Still, it helps to identify eventual incompatibilities that may arise. Therefore, we propose the CDLVT. It is a formal approach which aims to verify a series of non-functional properties. These latter are divided into two distinct classes: global and internal properties.
The global properties are checked for any invoked services in a given choreography. Whereas internal properties, they describe the different interdependence relationships between activities within a WS-CDL process.
To achieve our purpose and to implement our approach in a practical context, we propose a verification tool CDL2P. It takes, as input, the choreography specified in WS-CDL which will be automatically transformed into Spin-Promela. This transformation will keep the same semantics and the same features of WS-CDL activities in the Promela code.
After that, it will be time to check automatically, a set of properties which are already provided. So, we ensure via this tool the automatic generation of file which contains the different properties that will be verified later.
A choreography specification is translated into an abstract model, and the properties to be checked are encoded as logic formula. Then they are fed into a model checker. The latter may give a positive answer, or a negative one. It is noteworthy, that the transformation is based on grammar rules and relies on the principle of the XSLT processor operating.
Case Study
A service choreography specifies a communication protocol for all involved partners. In this composition model, the process definition is viewed from a global perspective. To better explain our purpose, we choose the typical scenario "shopping on line".
Thereby, we note that the realization of the main goal of this business process is divided between different elementary choreographies.
In case of shopping online, the different partners involved in this choreography are: the shipper, the client, the credit-check agency and the seller. Indeed, the process begins when the client requests a quote from the seller. The latter replied to the request which can be either accepted or rejected by the customer. On acceptance, the customer fills out a form containing command information to perform (name, address, quantity, etc.) and sends it to the seller. Then, the seller requests the agency credit check agency to verify the validity of the customer's card. If the card is rejected, the credit check agency sends a refusal to customer through the seller. In this case, the process is ended. If the card is accepted, the seller confirms the order and passes a request for delivery to the shipper. If the latter accepts the request, it retrieves the necessary information from the seller to send the delivery to the customer. Note that an updated estimate may be requested by the buyer and accepted by the seller.
Overview
We outline, throughout these documents, the whole transformation. We are based on WS-CDL specification to reach a Promela process by applying XSLT rules.
Demo
We have conceived a tool CDLVT which takes in input a WS-CDL specification which will be transformed, in turn, to SPIN-Promela. And here is a video demonstration of our proposed tool
Contributors
Sirine REBAI
- si.rebai@gmail.com
Mohamed Karâa
- mohammed.karaa@gmail.com
Hatem Hadj Kacem
- Hatem.Hadjkacem@fsegs.rnu.tn
