PiFF: A formal framework for dynamic service composition

Service choreography and orchestration are two views of the service compositions. In order to select and compose services correctly, some formal methods and tools are used to model and verify those compositions. Pi calculus is a major theory of process algebra that can be used as the formal basis of service composition. According to analysis result of WS CDL and WS BPEL, PiFF - a formal verification framework based on pi calculus is proposed which can be used to check and validate service composition both from global and local point of views. PiFF constitutes of three parts: mapping, methods and tools. This framework can promise consistency between WS CDL and WS BPEL and guarantee developing of dynamic service composition correctly by concept of weak bisimulation.