Abstract—Web service-business process execution Language (WS-BPEL) is a promising language for describing a
web service composition. Unfortunately, WS-BPEL lacks expressive power of formal semantics to support verifiability. Consequently, timed trace theory has been used to assure the
correctness and reliability of the web service composition with timing constraints. Moreover, since most of business processes are more complicated, the cost of verification is high. It is likely
that the state explosion problem will take place. In order to
tackle this problem, in this paper a partial order reduction algorithm for timed trace theoretic verification has been applied to minimize the number of states. Experimenting with a
tourism information system, the proposed approach expresses
its effectiveness.
Index Terms—Partial order reduction, timed trace theory,
web service composition.
The authors are with the Department of Computer Science, Thammasat
University, Pathumthani, Thailand (e-mail: denduang@cs.tu.ac.th;
oatt_fanclub@hotmail.com).
[PDF]
Cite: Denduang Pradubsuwun and Wutthipong Kongburan, "Partial Order Reduction for Verification of WS-BPEL," International Journal of Modeling and Optimization vol. 4, no. 3, pp. 239-245, 2014.