Abstract
WS-Business Activity specification defines two coordination protocols in order to ensure a consistent agreement on the outcome of long-running distributed applications. We use the model checker Uppaal to analyse the Business Agreement with Coordination Completion protocol type. Our analyses show that the protocol, as described in the standard specification, violates correct operation by reaching invalid states for all underlying communication media except for the perfect FIFO. Based on this result, we propose changes to the protocol. A further investigation of the modified protocol suggests that messages should be received in the same order as they are sent so that a correct protocol behaviour is preserved. Another important property of communication protocols is that all parties always reach their final states. Based on the verification with different communication models, we prove that our enhanced protocol satisfies this property for asynchronous, unreliable, order-preserving communication whereas the original protocol does not.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Afek, Y., Attiya, H., Fekete, A., Fischer, M., Lynch, N., Mansour, Y., Wang, D.-W., Zuck, L.: Reliable communication over unreliable channels. J. ACM 41(6), 1267–1297 (1994)
Apt, K.R., Francez, N., Katz, S.: Appraising fairness in languages for distributed programming. Distributed Computing 2, 226–241 (1988)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM 30(2), 323–342 (1983)
Gray, J., Reuter, A.: Transaction Processing: Concepts and Techniques. Morgan Kaufmann, San Francisco (1993)
Greenfield, P., Kuo, D., Nepal, S., Fekete, A.: Consistency for web services applications. In: VLDB 2005: Proceedings of the 31st International Conference on Very Large Data Bases, pp. 1199–1203. VLDB Endowment (2005)
Johnson, J.E., Langworthy, D.E., Lamport, L., Vogt, F.H.: Formal specification of a web services protocol. Journal of Logic and Algebraic Programming 70(1), 34–52 (2007)
Lamport, L.: Specifying Systems. Addison-Wesley, Reading (2003)
Mathew, B., Juric, M., Sarang, P.: Business Process Execution Language for Web Services, 2nd edn. Packt Publishing (2006)
Newcomer, E., Robinson, I. (chairs): Web services atomic transaction (WS-atomic transaction) version 1.2 (2009), http://docs.oasis-open.org/ws-tx/wstx-wsat-1.2-spec.html
Newcomer, E., Robinson, I. (chairs): Web services business activity (WS-businessactivity) version 1.2 (2009), http://docs.oasis-open.org/ws-tx/wstx-wsba-1.2-spec-os/wstx-wsba-1.2-spec-os.html
Newcomer, E., Robinson, I. (chairs): Web services coordination (WS-coordination) version 1.2 (2009), http://docs.oasis-open.org/ws-tx/wstx-wscoor-1.2-spec-os/wstx-wscoor-1.2-spec-os.html
Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: Theory and application. Information and Computation 114(1), 131–178 (1994)
Ravn, A.P., Srba, J., Vighio, S.: UPPAAL model of the WS-BA protocol, Available in the UPPAAL example section at http://www.uppaal.org
Ravn, A.P., Srba, J., Vighio, S.: A formal analysis of the web services atomic transaction protocol with uppaal. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 579–593. Springer, Heidelberg (2010)
Robinson, I.: Answer in WS-BA discussion forum, July 14 (2010), http://markmail.org/message/wriewgkboaaxw66z
Vogt, F.H., Zambrovski, S., Gruschko, B., Furniss, P., Green, A.: Implementing web service protocols in SOA: WS-coordination and WS-businessactivity. In: Proceedings of the Seventh IEEE International Conference on E-Commerce Technology Workshops (CECW 2005), pp. 21–28. IEEE Computer Society, Los Alamitos (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ravn, A.P., Srba, J., Vighio, S. (2011). Modelling and Verification of Web Services Business Activity Protocol. In: Abdulla, P.A., Leino, K.R.M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2011. Lecture Notes in Computer Science, vol 6605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19835-9_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-19835-9_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19834-2
Online ISBN: 978-3-642-19835-9
eBook Packages: Computer ScienceComputer Science (R0)