Abstract
Designing web services-based processes (WSP) requires striking the balance between intuitive and easy to understand process representation for the interactive domain user and consolidated formal mathematical specification. An easy to understand process representation facilitates conformance of process correctness where as the formal mathematical specification ensures formal verification of service orchestration for executing the process. Orchestration of services involves overall service design, service selection, and composition of services to achieve the overall goal. In this paper we present a novel approach to service orchestration that combines an effective diagrammatic modeling, an appropriate formal framework and an implementation process for dynamic WSP and complex web service composition and verification. Specifically we introduce a new approach for WSP design and verification comprising of service orchestration using High Level Message Sequence Charts (HMSC) and Colored Petri Nets (CP Nets) that provides a methodology for analysis and verification at a process level as well as the service level.