摘要:Web services are available applications on the Web which can be invoked by users to accomplish a potentially business task. However, to meet user’s requirements, it becomes necessary to dynamically organize existent services and combine them, responding thus to a new purpose. In this paper, we propose a methodology called WS-mcv (Web Service Modeling, Composing and Verifying) that addresses the main problems arising in Web service composition area. WS-mcv represents an efficient and modular multistep approach achieved by breaking service composition into three processes: service modeling, automatic composition and formal verification. The proposed methodology makes use of the G-Net framework to allow an easiest modeling of basic and existent services. We propose a collection of expressive G-Net based operators that successfully solves complex Web service composition. WS-mcv also defines means to ensure composition correctness. All the processes of WS-mcv have been successfully automated in a model transformation based visual environment.