A process algebra for environment-based specification of web services

It is now well-accepted that formal methods are helpful for many problems raised in Web Service area. In this paper, we propose a new process algebra to formalize the environment-based specification of Web Services. From our point of view, the capability of a Web Service is considered in terms of the effects it imposes on the environment during its execution. The environment is composed of numbers of environment entities. For each entity, we first use the algebraic specification language CASL to describe its data(static) aspect, and then use our new process algebra to formally specify its dynamic behavior aspect. Based on that, a Web Service is specified as a process, and we can easily characterize its interaction with the environment. Furthermore, a behavior equivalence between two web services is established by using the notion of strong bisimulation in the new process algebra, some important properties of this relation are proved as well.