Toward a better Interoperability of Enterprise Information Systems: A CPNs and Timed CPNs -based Web Service Interoperability Verification in a Choreography

Service-Oriented Architectures (SOA) claim to facilitate the construction of flexible and loosely coupled business applications. Therefore it is seen as an enabling factor for the interoperability of Enterprise Information Systems (EIS). Web services are currently the most promised concretization of SOA. This concept is currently carried further to address the composition of individual services through orchestration and choreography in order to automate a business process allowing enterprises to develop value added products. Web service choreographies are more collaborative in nature and permit direct interactions between Web services. In order to have a better interoperability of EIS, a good behavior and an efficiency of Web service choreography is necessary. This paper addresses the raised issues by providing a process of Web service choreography. The originality of this process is the formal verification of the service interoperability basing on formal methods and tools, especially Colored Petri Nets (CPNs) and Timed CPNs formal specification languages, and model checking and simulation techniques. This formal verification is done at design time, which is an important step towards reliable Web service choreography, since problems could be detected early in the development cycle before even starting the implementation. It aims to prove that Web service choreography is correct in terms on message ordering constraints and efficient in terms of time constraints. This originality reflects the reality of enterprises interoperability that depends not only on qualitative constraints (message ordering) but also on quantitative ones such as time. The effectiveness of work has been validated using the recent version of CPN Tools. (C) 2014 The Authors. Published by Elsevier Ltd.