Design and Verification ofWeb Services Compositions in the Telecommunication Domain

Telecommunication is a key area where the use of web services has an enormous potential to facilitate the development of powerful and complex functionalities on top of existing ones. At the same time, the specific features of TelCo applications (asynchronous, event-driven communications, handling concurrent, long-running transactions, dynamically evolving sets of partners) pose difficult challenges to the adoption of standard languages and tools for web services. In this work, based on our analysis of TelCo standards and applications, we discuss a set of orchestration patterns, and show how these can be modeled using the WS-BPEL language. We also address the issue of guaranteeing the correctness of such applications, providing an automated support for the formal analysis of their behavior.