Abstract
Concerned with Web service composition, this paper proposes a model checking method of verifying asynchronous communication behaviors and timed properties. Firstly, analyzing Web service composition from software architecture, the interactive behaviors and timed properties are described by XYZ/ADL based on temporal logic language. Secondly, timed asynchronous communication model (TACM) which accords with the specification of model checker UPPAAL is proposed. Finally, based on the transition from XYZ/RE communication commands to TACM, the correctness of asynchronous communication behaviors of the service composition system can be verified by UPPAAL.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Pistore, M., Roveri, M., Busetta, P.: Requirements-driven verification of Web services. In: WSFM 2004, pp. 95–108 (2004)
Lei, L.H., Duan, Z.H.: An extended deterministic finite automata based method for the verification of composite Web services. Journal of Software 18(12), 2980–2990 (2007) (in Chinese)
Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based verification of Web service compositions. In: IEEE ASE 2003, pp. 152–161 (2003)
Fu, X., Bultan, T., Su, J.: Synchronizability of conversations among Web services. IEEE Transactions on Software Engineering 31(12), 1042–1055 (2005)
Pallickara, S., Fox, G., Pallickara, S.L.: An analysis of reliable delivery specifications for Web services. In: 10th International Conference on Information Technology: Coding and Computing, pp. 360–365 (2005)
Vieira, H.T., Caires, L., Seco, J.C.: The conversation calculus: A model of service oriented computation. In: 17th European Symposium on Programming, pp. 269–283 (2008)
Zhang, G.Q., Rong, M., He, Y.L., Zhu, X.Y., Yan, R.J.: A refinement checking method of Web service composition. In: IEEE SOSE 2010, pp. 103–106 (2010)
Tang, Z.S., et al.: Temporal logic programming and software engineering. Science Press, Beijing (2002) (in Chinese)
Guermouche, N., Godart, C.: Timed model checking based approach for Web services analysis. In: IEEE ICWS 2009, pp. 213–221 (2009)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
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
Zhang, G., Shi, H., Rong, M., Di, H. (2011). Model Checking for Asynchronous Web Service Composition Based on XYZ/ADL. In: Gong, Z., Luo, X., Chen, J., Lei, J., Wang, F.L. (eds) Web Information Systems and Mining. WISM 2011. Lecture Notes in Computer Science, vol 6988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23982-3_52
Download citation
DOI: https://doi.org/10.1007/978-3-642-23982-3_52
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23981-6
Online ISBN: 978-3-642-23982-3
eBook Packages: Computer ScienceComputer Science (R0)