This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
From Web Service Artifact to a Readable and Verifiable Model
October-December 2009 (vol. 2 no. 4)
pp. 277-288
John C. Sloan, Florida Atlantic University , Boca Raton
Taghi M. Khoshgoftaar, Florida Atlantic University , Boca Raton
Models of Web service compositions that are both readable and verifiable will benefit organizations that integrate purportedly reusable Web services. Colored Petri nets (CPNs) are at once verifiable and visually expressive, capable of presenting subtle flaws in service composition. Constructing CPN models from Business Process Execution Language (BPEL) artifacts had been a manual process requiring human judgment. Building on results from the Workflow Community, we automate the mapping of artifacts written in BPEL to models used by CPN Tools—a formal verification environment for development, simulation, and model checking of colored Petri nets. We extend related work that already converts BPEL to Petri nets, to reflect hierarchy and data type (color in CPN terminology), while improving model layout. We present a prototype implementation that mines both a BPEL artifact and the Petri net generated from it by an existing tool. The prototype partitions the Petri net into subnets, lays them out, colors them, and generates their XML file for import into CPN Tools. Our results include depictions of subnets produced and initial simulation results for a well-known case study.

[1] A. Alves, A. Arkin, S. Askary, C. Barreto, B. Bloch, F. Curbera, M. Ford, Y. Goland, A. Guízar, N. Kartha, C.K. Liu, R. Khalaf, D. König, M. Marin, V. Mehta, S. Thatte, D. van der Rijn, P. Yendluri, and A. Yiu, Web Services Business Process Execution Language Version 2.0, http://docs.oasis-open.org/wsbpel/2.0/OS wsbpel-v2.0-OS.html, Apr. 2007.
[2] G.D. Battista, P. Eades, R. Tamassia, and I.G. Tollis, Graph Drawing—Algorithms for the Visualization of Graphs. Prentice Hall, 1999.
[3] G. Behrmann, A. David, and K.G. Larsen, “A Tutorial on UPPAAL,” Formal Methods for the Design of Real-Time Systems, M.Bernardo and F. Corradini, eds., pp. 200-236, Springer, 2004.
[4] J. Billington, S. Christensen, K.M. van Hee, E. Kindler, O. Kummer, L. Petrucci, R. Post, C. Stehno, and M. Weber, “The Petri Net Markup Language: Concepts, Technology, and Tools,” Proc. 24th Int'l Conf. Applications and Theory of Petri Nets (ICATPN '03), pp. 483-505, Springer, 2003.
[5] J.M. Boyer, “A New Method for Efficiently Generating Planar Graph Visibility Representations,” Graph Drawing, P. Healy and N.S. Nikolov, eds., pp. 508-511, Springer, 2005.
[6] F.R.K. Chung, F.T. Leighton, and A.L. Rosenberg, “Embedding Graphs in Books: A Layout Problem with Applications to VLSI Design,” Graph Theory with Applications to Algorithms and Computer Science, Y. Alavi, G. Chartrand, L. Lesniak, D.R. Lick, and C.E.Wall, eds., pp. 175-188, John Wiley & Sons, 1985.
[7] H. Foster, S. Uchitel, J. Magee, and J. Kramer, “LTSA-WS: A Tool for Model-Based Verification of Web Service Compositions and Choreography,” Proc. 28th Int'l Conf. Software Eng. (ICSE '06), pp.771-774, 2006.
[8] X. Fu, T. Bultan, and J. Su, “WSAT: A Tool for Formal Analysis of Web Services,” Computer Aided Verification, R. Alur and D. Peled, eds., pp. 510-514, Springer, 2004.
[9] X. Fu, T. Bultan, and J. Su, “Synchronizability of Conversations among Web Services,” IEEE Trans. Software Eng., vol. 31, no. 12, pp. 1042-1055, Dec. 2005.
[10] X. He and H. Zhang, “Nearly Optimal Visibility Representations of Plane Graphs,” SIAM J. Discrete Math., vol. 22, no. 4, pp. 1364-1380, 2008.
[11] G.J. Holzmann, “The Logic of Bugs,” Proc. 10th ACM SIGSOFT Symp. Foundations of Software Eng. (SIGSOFT '02/FSE-10), pp. 81-87, 2002.
[12] J.E. Hopcroft and R.E. Tarjan, “Efficient Planarity Testing,” J.ACM, vol. 21, no. 4, pp. 549-568, 1974.
[13] K. Jensen, L.M. Kristensen, and L. Wells, “Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems,” Int'l J. Software Tools for Technology Transfer (STTT), vol. 9, nos. 3/4, pp. 213-254, 2007.
[14] W. jun Li, X. jun Liang, H. mei Song, and X. cong Zhou, “QoS-Driven Service Composition Modeling with Extended Hierarchical CPN,” Proc. First Joint IEEE/IFIP Symp. Theoretical Aspects of Software Eng. (TASE '07), pp. 483-492, 2007.
[15] N. Lohmann, P. Massuthe, C. Stahl, and D. Weinberg, “Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation,” Data & Knowledge Eng., vol. 64, no. 1, pp. 38-54, 2008.
[16] J. Magee and J. Kramer, Concurrency: State Models and Java Programs, second ed. Wiley, 2006.
[17] J. Mendling, C.P. de Laborda, and U. Zdun, “Towards an Integrated BPM Schema: Control Flow Heterogeneity of PNML and BPEL4WS,” Wissensmanagement, K.-D. Althoff, A. Dengel, R.Bergmann, M. Nick, and T. Roth-Berghofer, eds., pp. 570-579, Springer, 2005.
[18] C. Ouyang, E. Verbeek, W.M.P. van der Aalst, S. Breutel, M. Dumas, and A.H.M. ter Hofstede, “Formal Semantics and Analysis of Control Flow in WS-BPEL,” Science of Computer Programming, vol. 67, nos. 2/3, pp. 162-198, 2007.
[19] A.V. Ratzer, L. Wells, H.M. Lassen, M. Laursen, J.F. Qvortrup, M.S. Stissing, M. Westergaard, S. Christensen, and K. Jensen, “CPN Tools for Editing, Simulating, and Analysing Coloured Petri Nets,” Proc. 24th Int'l Conf. Applications and Theory of Petri Nets (ICATPN '03), pp. 450-462, 2003.
[20] B.-H. Schlingloff, A. Martens, and K. Schmidt, “Modeling and Model Checking Web Services,” Electronic Notes Theoretical Computer Science, vol. 126, pp. 3-26, 2005.
[21] J.C. Sloan, T.M. Khoshgoftaar, and V. Raghav, “Assuring Timeliness in an E-Science Service-Oriented Architecture,” Computer, vol. 41, no. 8, pp. 56-62, Aug. 2008.
[22] Proc. 24th Int'l Conf. Applications and Theory of Petri Nets (ICATPN '03), W.M.P. van der Aalst and E. Best, eds. Springer, June 2003.
[23] Q. Wu, C. Pu, and A. Sahai, “DAG Synchronization Constraint Language for Business Processes,” Proc. Third IEEE Int'l Conf. E-Commerce Technology, pp. 10-17, 2006.
[24] Y. Yang, Q. Tan, J. Yu, and F. Liu, “Transformation BPEL to CP-Nets for Verifying Web Services Composition,” Proc. Int'l Conf. Next Generation Web Services Practices (NWESP '05), pp.137-142, 2005.

Index Terms:
Web services, Petri nets, formal verification, graph drawing.
Citation:
John C. Sloan, Taghi M. Khoshgoftaar, "From Web Service Artifact to a Readable and Verifiable Model," IEEE Transactions on Services Computing, vol. 2, no. 4, pp. 277-288, Oct.-Dec. 2009, doi:10.1109/TSC.2009.23
Usage of this product signifies your acceptance of the Terms of Use.