Abstract
Current Web services composition proposals, such as BPEL, BPSS, BPMN and WSCI, provide notations for describing the control and message flows in Web service collaborations. However, such proposals remain at the descriptive level, without providing any kind of mechanisms or tool support for verifying the composition specified in the proposed notations. In this paper, we present to analyze and verify Web services composition by using CP-nets. CP-nets combine the strengths of Petri nets with the expressive power of high-level programming and have sound mathematical semantics. These services composition proposals can be transformed by model transformation rules into CP-nets, which can be used to analyze the performance and to investigate behavioral properties by CP-nets specialized tools.
The paper is partially supported by the National Natural Science Foundation of China under Grant No.90104007, 60233020; the National High-Tech Research and Development Plan of China (863) under Grant No.2001AA113202, 2001AA113190, 2003AA001023.
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.
Similar content being viewed by others
References
Jensen, K.: Colored Petri Nets Basic Concepts, Analysis Methods and Practical Use, 2nd edn. EATCS Monographs on Theoretical Computer Science, vol. 1, 2, 3. Springer, Heidelberg (1997)
Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based verification of web service composition. In: Proceedings of the Eighteenth IEEE International Conference on Automated Software Engineering (ASE 2003), pp. 152–162. IEEE Computer Society Press, Los Alamitos (2003)
Nakajima, S.: Verification of Web Service Flows with Model-Checking Techniques. In: Proceedings of the First International Symposium on Cyber Worlds (CW 2002), pp. 378–385. IEEE Computer Society Press, Los Alamitos (2002)
Karamanolis, C., Giannakopoulou, D., Magee, J., Wheater, S.M.: Model checking of workflow schemas. In: Proceedings of the 4th International Enterprise Distributed Object Computing Conference (EDOC 2000), pp. 170–179. IEEE Computer Society Press, Los Alamitos (2000)
Visser, W., Havelund, K., Brat, G., Spark, S., Lerda, F.: Model checking programs. In: Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE 2000), pp. 203–232. IEEE Computer Society Press, Los Alamitos (2000)
Koehler, J., Tirenni, G., Kumaran, S.: From business process model to consistent implementation: a case study for formal verification methods. In: Proceedings of the 6th International Enterprise Distributed Object Computing Conference (EDOC 2002), pp. 96–106. IEEE Computer Society Press, Los Alamitos (2002)
Koshkina, M.: Verification of business processes for web services. Master’s thesis, York University (2003)
van der Aalst, W.M.P.: Verification of workflow nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 407–426. Springer, Heidelberg (1997)
Martens, A.: Distributed Business Processes – Modeling and Verification by help of Web Services. PhD thesis, Humboldt-Universität zu Berlin (July 2003), Available at http://www.informatik.hu-berlin.de/top/download/documents/pdf/Mar03.pdf
Narayanan, S., McIlraith, S.: Analysis and simulation of Web services. Special issue: The Semantic Web: an evolution for a revolution. Computer Networks: The International Journal of Computer and Telecommunications Networking 42, 675–693 (2003)
Stahl, C.: Transformation von BPEL4WS in Petrinetze. Diplomarbeit, Humboldt-UniversitÄat zu Berlin (April 2004)
Varró, D., Pataricza, A.: Automated Formal Verification of Model Transformations. In: Proceedings of Workshop on Critical Systems Development with UML (CSDUML 2003), Technische Universitat Munchen, pp. 63–78 (2003)
Yang, Y., Tan, Q., Yu, J., Liu, F.: Transformation BPEL to CP-Nets for Verifying Web services Composition. To appear in proceedings of the International Conference on Next generation Web services Practices (NWeSP 2005). IEEE Computer Society Press, Los Alamitos (2005)
Yang, Y., Tan, Q., Xiao, Y.: Verifying Web Services Composition. To appear in proceedings of eCOMO workshop of the 24th International Conference on Conceptual Modeling (ER 2005), pp. 358–367. Springer, Heidelberg (2005)
Yang, Y., Tan, Q., Xiao, Y.: Verifying Web Services Composition Based on Hierarchical Colored Petri Nets. To appear in proceedings of IHIS workshop of the 14th ACM Conference on Information and Knowledge Management (CIKM 2005). ACM, New York (2005)
Miller, R.J., Ioannidis, Y.E., Ramakrishnan, R.: The Use of Information Capacity in Schema Integration and Translation. In: Agrawal, R., Baker, S., Bell, D.A. (eds.) Proceedings of the 19th Very Large Data Bases Conference, pp. 120–133. Morgan Kaufmann, San Francisco (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yang, Y., Tan, Q., Xiao, Y. (2005). Model Transformation Based Verification of Web Services Composition. In: Zhuge, H., Fox, G.C. (eds) Grid and Cooperative Computing - GCC 2005. GCC 2005. Lecture Notes in Computer Science, vol 3795. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590354_8
Download citation
DOI: https://doi.org/10.1007/11590354_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30510-1
Online ISBN: 978-3-540-32277-1
eBook Packages: Computer ScienceComputer Science (R0)