Business Transaction Verification-enabled Service Coordination Model
Li Xiang · Journal of Chinese Computer Systems · 2011
It is an urgent issue how to ensure distributed agreement among multiple-participants of service composition and business process.The definition of the message exchanges that take place between the process and each one of its partners in WS-TX OASIS Standard lacks the precise definition which is required for describing complex coordinated activities.This paper first models WS-Business Activity protocol(WS-BA) which specifies coordination types for long running loosely coupled business transactions.Second,proposes a service coordination model based on the formalization of the messaging interactions semantics in WS-BA using Pi-calculus.Then verifies system whether the protocol satisfies safety and liveness with HAL model checker.Finally,a case study of business transaction verification in multi-participants coordination is also presented,and introduces how to analyze the correctness of design for business process using model checking technology in order to efficiently guarantee the consistency and reliability of business transactions.