Abstract
The success of the cloud computing initiative is heavily dependent on realizing trustworthy Web Services. The trustworthiness of a Web Service is judged by four factors: security, privacy, reliability and business integrity. Web Services use message-passing for communication which opens the door for messages races. Messages race with each other when their order of arrival at a destination is not guaranteed and is affected non-deterministically by factors such as network latencies and scheduling variations. Message races are dangerous to Web Services because they can be unforeseen consequences of bugs, causing messages to arrive in an unexpected ordering. In this paper we present a novel approach for improving the reliability of Web Services by detecting message races using SMT-based analysis. We model a BPEL process as a Web Service Modeling Graph (WSMG). A WSMG model is then encoded into a set of SMT constraints. The satisfiability of these constraints means that message races will occur during the actual execution of the Web Service. Hence, we reduce the message race detection problem to constraint solving problem based on satisfiability modulo theories (SMT).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Schneider, F.B.: Trust in Cyberspace. National Academies Press, Washington (1999)
Christey, S. (eds), Top 25 most dangerous programming errors, CWE/SANS report (2009), http://cwe.mitre.org/top25
Klein, J., Leymann, F., Roller, D., Curbera, F., Goland, Y., Weerawarana, S.: Business process execution language for web services, version 1.1 (2003)
Satisfiability Modulo Theories, http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506–521 (1999)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: 38th Design Automation Conference (DAC), pp. 530–535. ACM Press, New York (2001)
Een, N., Sorensson, N.: An extensible sat-solver. In: Satisfiability Workshop, pp. 333–336 (2003)
Dutertre, B., de Moura, L.: Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Moura, L.D., Bjrner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Netzer, R.H.B., Miller, B.P.: Optimal tracing and replay for debugging message-passing parallel programs. In: Super computing 1992: Proceedings of the 1992 ACM/IEEE conference on Supercomputing, pp. 502–511. IEEE Computer Society Press, Los Alamitos (1992)
Netzer, R.H.B., Brennan, T.W., Damodaran-Kamal, S.K.: Debugging race conditions in message-passing programs. In: SPDT 1996: Proceedings of the SIGMETRICS symposium on Parallel and distributed tools, pp. 31–40. ACM Press, New York (1996)
Park, M.Y., Shim, S.J., Jun, Y.K., Park, H.R.: Mpirace-check: Detection of message races in MPI programs. In: Cérin, C., Li, K.-C. (eds.) GPC 2007. LNCS, vol. 4459, pp. 322–333. Springer, Heidelberg (2007)
Weiss, M., Esfandiari, B.: On feature interactions among web services. In: IEEE International Conference on Web Services. IEEE Computer Society, Los Alamitos (2004)
Zhang, J., Su, S., Yang, F.: Detecting race conditions in web services. In: AICT ICIW 2006: Proceedings of the Advanced Int’l Conference on Telecommunications and Int’l Conference on Internet and Web Applications and Services, p. 184. IEEE Computer Society, Washington (2006)
Zhang, J., Yang, F., Su, S.: Detecting feature interactions in web services with model checking techniques. The Journal of China Universities of Posts and Telecommunications 14(3), 108–112 (2007)
Alur, R., NcDougall, M., Yang, Z.: Exploiting Behavioral Hierarchy for Efficient Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 338. Springer, Heidelberg (2002)
Elwakil, M., Yang, Z., Liqiang, W.: CRI: Symbolic Debugger for MCAPI Applications. In: Chin, W.-N. (ed.) ATVA 2010. LNCS, vol. 6252, pp. 353–358. Springer, Heidelberg (2010)
Elwakil, M., Yang, Z.: Debugging Support Tool for MCAPI Applications. In: Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD - VIII). ACM, Trento (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Elwakil, M., Yang, Z., Wang, L., Chen, Q. (2010). Message Race Detection for Web Services by an SMT-Based Analysis. In: Xie, B., Branke, J., Sadjadi, S.M., Zhang, D., Zhou, X. (eds) Autonomic and Trusted Computing. ATC 2010. Lecture Notes in Computer Science, vol 6407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16576-4_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-16576-4_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16575-7
Online ISBN: 978-3-642-16576-4
eBook Packages: Computer ScienceComputer Science (R0)