SpringerLink
Log in

Service Modelling and Verification: A Formal Approach

  • Chapter
  • First Online:
Webservices

Abstract

Increasing number of users on web has attracted a large number of businesses to be made available on web. The growing demand for webservices requires a systematic approach in service development. For the purpose, this chapter reviews various models for service specification, composition, deployment and monitoring. Particularly, the chapter reviews some well-known models like UML, Petrinet and state machine used for service modelling and verification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 89.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 119.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Irum Rauf. Muhammad Zohaib Z Iqbal, Zafar. I. Malik UML based Modeling of Web Service Composition- A Survey; Sixth International Conference on Software Engineering Research, Management and Applications, 2008

    Google Scholar 

  2. Christophe Dumez, Ahmed Nait-Sidi-Moh, Jaafar Gaber, Maxime Wack, Modelling and specification of Web services composition using UML-S, 4th international conference on Next Generation Web Services Practices (NWeSP08), Oct 2008, Seoul, South Korea. IEEE Computer Society, 0, pp. 15–20

    Google Scholar 

  3. Dhikra Kchaou, WS-UML: A UML Profile for Web Service Applications, ISIICT’09 Proceedings of the Third international conference on Innovation and Information and Communication Technology, British Computer Society Swindon, UK, 2009

    Google Scholar 

  4. Pengcheng Zhang, Henry Muccini; Model and Verification of WS-CDL based on UML Diagrams; International Journal of Software Engineering and Knowledge Engineering Vol. 20, No. 8 (2010) 1119–1149

    Google Scholar 

  5. M. Emilia Cambronero J. Jose Pardo Gregorio Diaz Valentin Valero; Using RT-UML for Modelling Web Services; SAC07 March 11–15, 2007, Seoul, Korea

    Google Scholar 

  6. Viet-Cuong Nguyen, Xhevi Qafmolla, Karel Richta; Domain Specific Language Approach on Model-driven Development of Web Services; Acta Polytechnica Hungarica Vol. 11, No. 8, 2014, 121–138

    Google Scholar 

  7. W. Provost, “UML for Web services”, XML.com, August 5, 2003

    Google Scholar 

  8. Jun-Jang Jeng, Wang-Chuan Tsai; Designing An FSM Architectural Framework for Service-Based Applications; COMPSAC, 2000, pp. 234–239

    Google Scholar 

  9. R. Gronmo, I. Solheim, “Towards Modeling Web Service Composition in UML”, INSTICC Press, 2nd International Workshop on web services: Modeling, Architecture and Infrastructure, Porto, Portugal, April 2004

    Google Scholar 

  10. F. Belouadha and O. Roudiés, « Vers un modèle de spécification pour la composition de services web », Proceedings of SIIE’08, Tunisie, Février 2008

    Google Scholar 

  11. G. Ortiz and J. Hernandez, “Toward UML Profiles for web services and their Extra-functional Properties”, IEEE International Conference on Web services (ICWS’06), 2006

    Google Scholar 

  12. F. Belouadha and O. Roudiés, “Un profil UML de spécification de services web composites sémantiques”, CARI 2008-MAROC, pp. 537–544

    Google Scholar 

  13. Jia Zhang, Carl K. Chang, Jen-Yao Chung, Seong W. Kim; WS-Net: A Petri-net Based Specification Model for Web Services; Proceedings of the IEEE International Conference on Web Services (ICWS04)

    Google Scholar 

  14. Yudith Cardinale, Joyce El Haddad, Maude Manouvrier, Marta Rukoz; Web Service Composition Based on Petri Nets: Review and Contribution; LNCS 8194, pp. 83–122, 2013

    Google Scholar 

  15. Sofiane Chemaa, Faycal Bachtarzi, Allaoua Chaoui; A high-level Petri net based approach for modeling and composition of web services; Procedia Computer Science 9 (2012) 469–478

    Google Scholar 

  16. Y. Deng, S. K. Chang, J. C. A. De Figueiredo, A. Psrkusich, Integrating software engineering methods and petri nets for the specification and prototy** of complex information systems, in: Proc. The 14th International Conference on Application and Theory of Petri Nets, Chicago, 1993, pp. 206–223

    Google Scholar 

  17. Hamadi, R., Benatallah, B.: A Petri net-based Model for Web Service Composition. In: Proc. of the 14th Australasian Database Conf., ADC 2003, vol. 17, pp. 191–200

    Google Scholar 

  18. Zhang, Z., Hong, F., **ao, H.: A colored petri net-based model for web service composition. Journal of Shanghai University (English Edition) 12, 323–329 (2008)

    Google Scholar 

  19. Yu, H., Fan, G., Chen, L., Liu, D.: Analyzing time constrained service composition based on Petri net. In: 3rd Int. Symposium on Electronic Commerce and Security Workshops, pp. 68–71 (2010)

    Google Scholar 

  20. Fang, X., Jiang, C., Fan, X.: Independent global constraints for web service composition based on GA and APN. In: Proc. of the First ACM/SIGEVO Summit on Genetic and Evolutionary Computation, GEC 2009, pp. 119–126 (2009)

    Google Scholar 

  21. Hinz, S., Schmidt, K., Stahl, C.: Transforming BPEL to Petri nets. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol. 3649, pp. 220–235. Springer, Heidelberg (2005)

    Google Scholar 

  22. Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing interacting WSBPEL processes using flexible model generation. Data Knowl. Eng. 64(1), 38–54 (2008)

    Google Scholar 

  23. Ouyang, C., Verbeek, E., van der Aalst, W.M.P., Breutel, S., Dumas, M., ter Hofstede, A.H.M.: Formal semantics and analysis of control flow in WS-BPEL. Sci. Comput. Program. 67(2–3), 162–198 (2007)

    Google Scholar 

  24. Martens, A.: Analyzing Web Service Based Business Processes. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 19–33. Springer, Heidelberg (2005)

    Google Scholar 

  25. **ong, P., Fan, Y., Zhou, M.: A Petri Net Approach to Analysis and Composition of Web Services. IEEE Transact. on Systems, Man, and Cybernetics, Part A 40(2), 376–387 (2010)

    Google Scholar 

  26. Du, Y., Li, X., **ong, P.: A Petri Net Approach to Mediation-aided Composition of Web Services. IEEE Transactions on Automation Science and Engineering (2012) (to appear)

    Google Scholar 

  27. Li, X., Fan, Y., Sheng, Q.Z., Maamar, Z., Zhu, H.: A Petri Net Approach to Analyzing Behavioral Compatibility and Similarity of Web Services. IEEE Trans. on Systems, Man, and Cybernetics, Part A, 510–521 (2011)

    Google Scholar 

  28. Tan, W., Fan, Y., Zhou, M.: A Petri Net-Based Method for Compatibility Analysis and Composition of Web Services in Business Process Execution Language. IEEE T. Automation Science and Engineering 6(1), 94–106 (2009)

    Google Scholar 

  29. Chi, Y.-L., Lee, H.-M.: A formal modeling platform for composing web services. Expert Syst. Appl. 34(2), 1500–1507 (2008)

    Google Scholar 

  30. Ding, Z., Wang, J., Jiang, C.: An Approach for Synthesis Petri Nets for Modeling and Verifying Composite Web Service. J. Inf. Sci. Eng. 24(5), 1309–1328 (2008)

    Google Scholar 

  31. Yang, Y., Tan, Q., **ao, Y.: Verifying web services composition based on hierarchical colored petri nets. In: Proc. of the 1st Int. Workshop on Interoperability of Heterogeneous Information Systems, IHIS 2005, pp. 47–54 (2005)

    Google Scholar 

  32. Yang, Y., Tan, Q., **ao, Y., Liu, F., Yu, J.: Transform BPEL workflow into hierarchical CP-nets to make tool support for verification. In: Zhou, X., Li, J., Shen, H.T., Kitsuregawa, M., Zhang, Y. (eds.) APWeb 2006. LNCS, vol. 3841, pp. 275–284. Springer, Heidelberg (2006)

    Google Scholar 

  33. Dong, Y., **a, Y., Sun, T., Zhu, Q.: Modeling and performance evaluation of service choreography based on stochastic petri net. JCP 5(4), 516–523 (2010)

    Google Scholar 

  34. Mao, C.: Control Flow Complexity Metrics for Petri Net-based Web Service Composition. Journal of Software 5(11), 1292–1299 (2010)

    Google Scholar 

  35. **a, Y., Liu, Y., Liu, J., Zhu, Q.: Modeling and performance evaluation of bpel processes: A stochastic-petri-net-based approach. IEEE Trans. on Systems, Man, and Cybernetics, Part A 42(2), 503–510 (2012)

    Google Scholar 

  36. Bonchi, F., Brogi, A., Corfini, S., Gadducci, F.: Compositional Specification of Web Services Via Behavioural Equivalence of Nets: A Case Study. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol. 5062, pp. 52–71. Springer, Heidelberg (2008)

    Google Scholar 

  37. Thomas, J.P., Thomas, M., Ghinea, G.: Modeling of web services flow. In: IEEE Int. Conf. on E-Commerce (CEC), Stillwater, OK, USA, pp. 391–398 (2003)

    Google Scholar 

  38. Valero, V., Macià, H., Pardo, J.J., Cambronero, M.E., Díaz, G.: Transforming Web Services Choreographies with priorities and time constraints into prioritized-time colored Petri nets. Sci. Comput. Program. 77(3), 290–313 (2012)

    Google Scholar 

  39. Blanco, E., Cardinale, Y., Vidal, M.-E.: Aggregating Functional and Non-Functional Properties to Identify Service Compositions, pp. 1–36. IGI BOOK (2011)

    Google Scholar 

  40. Li, B., Xu, Y., Wu, J., Zhu, J.: A petri-net and qos based model for automatic web service composition. Journal of Software 7(1), 149–155 (2012)

    Google Scholar 

  41. Qian, Z., Lu, S., **e, L.: Colored Petri Net Based Automatic Service Composition. In: Proc. of the 2nd IEEE Asia-Pacific Service Computing Conf., pp. 431–438 (2007)

    Google Scholar 

  42. Cardinale, Y., El Haddad, J., Manouvrier, M., Rukoz, M.: CPN-TWS: a coloured petri-net approach for transactional-QoS driven Web Service composition. IJWGS 7(1), 91–115 (2011)

    Google Scholar 

  43. Cardinale, Y., Rukoz, M.: Fault Tolerant Execution of Transactional Composite Web Services: An Approach. In: Proceedings UBICOMM, Lisbon, Portugal, pp. 1–6 (2011)

    Google Scholar 

  44. Cardinale, Y., Rukoz, M.: A framework for reliable execution of transactional composite web services. In: MEDES, pp. 129–136 (2011)

    Google Scholar 

  45. Mei, X., Jiang, A., Li, S., Huang, C., Zheng, X., Fan, Y.: A Compensation Paired Net-based Refinement Method for Web Services Composition. Advances in Information Sciences and Service Sciences 3(4), 169–181 (2011)

    Google Scholar 

  46. Mei, X., Jiang, A., Zheng, F., Li, S.: Reliable Transactional Web Service Composition Using Refinement Method. In: Proc. of the 2009 WASE Int. Conf. on Information Engineering, ICIE 2009, vol. 01, pp. 422–426 (2009)

    Google Scholar 

  47. Wang, Y., Fan, Y., Jiang, A.: A paired-net based compensation mechanism for verifying Web composition transactions. In: 4th International Conference on New Trends in Information Science and Service Science (NISS), pp. 1–6 (2010)

    Google Scholar 

  48. Sukhamay Kundu; Modeling Complex Systems by A Set of Interacting Finite-State Models; APSEC, 2003, pp. 380–389

    Google Scholar 

  49. Basit Shafiq, Soon Chun, Jaideep Vaidya, Nazia Badar, Nabil Adam, Secure Composition of Cascaded Web Services, 8th International Conference Conference on Collaborative Computing: Networking, Applications and Worksharing, Collaboratecom 2012 Pittsburgh, PA, United States, October 14–17, 2012, 137–147

    Google Scholar 

  50. Andreas Wombacher, Peter Fankhauser, Bendick Mahleko; Matchmaking for Business Processes based on Choreographies; Proceedings of the 2004 IEEE International Conference on e-Technology, e-Commerce and e-Service

    Google Scholar 

  51. Conversation Specification: A New Approach to Design and Analysis of E-Service Composition; WWW2003, May 2024, 2003, 403–410

    Google Scholar 

  52. **ang Fu, Tevk Bultan, Jianwen Su; Analysis of Interacting BPEL Web Services; WWW2004, May 1722, 2004, New York, USA

    Google Scholar 

  53. **aochuan Yi and Krys J. Kochut, A CP-nets-based Design and Verification Framework for Web Services Composition, Proceedings of the IEEE International Conference on Web Services (ICWS04)

    Google Scholar 

  54. Yabei Wang, Shangliang Pan; CPN-Based Verification of Web Service Composition Model, Proc. International Conference on Educational and Information Technology, 2010, V1-153-158

    Google Scholar 

  55. Jesus Arias Fisteus, Luis Sanchez Fernandez, Carlos Delgado Kloos, Applying model checking to BPEL4WS business collaborations, Proc. of ACM Symposium on Applied Computing, 2005, 826–830

    Google Scholar 

  56. Zhang, Bixin Li, Henry Muccini, Yu Zhou, Mingjie Sun, Data-enriched Modeling and Verification of WS-CDL Based on UML Models; Zhang, Bixin Li, Henry Muccini, Yu Zhou, Mingjie Sun; Proc. on IEEE International Conference on Web Services, 2008, 752–754

    Google Scholar 

  57. Howard Foster, Sebastian Uchitel, Jeff Magee, Jeff Kramer, Model-based Verification of Web Service Compositions

    Google Scholar 

  58. Chun Ouyang, Eric Verbeek, Wil M.P. van der Aalst, Stephen Breutel, Marlon Dumas, and Arthur H.M. ter Hofstede, Formal Semantics and Analysis of Control Flow in WS-BPEL; Technical Report, Faculty of Information Technology, Queensland University of Technology, Australia

    Google Scholar 

  59. Melliti Tarek, Celine Boutrous-Saab, Sylvain Rampacek; Verifying correctness of Web services choreography, Technical Report, IBISC, University of Evry, France … Find reference details

    Google Scholar 

  60. Huiqun Zhao, **g Sun, **aodong Liu; A Model Checking Based Approach to Automatic Test Suite Generation for Testing Web Services and BPEL, Proc. of IEEE Asia-Pacific Services Computing Conference, 2012, 61–69

    Google Scholar 

  61. Zhuqing Li, Dianfu Ma, Yongwang Zhao, **g Li, Qing Yang; FSM4WSR: A Formal Model for Verifiable Web Service Runtime; Proc. of IEEE Asia-Pacific Services Computing Conference, 2011, pp. 86–93

    Google Scholar 

  62. Quan Z. Sheng, Zakaria Maamar, Lina Yao, Claudia Szabo, Scott Bourne, Behavior modeling and automated verification of Web services, Inform. Sci. (2012)

    Google Scholar 

  63. Walid Gaaloul, Sami Bhiri, and Mohsen Rouached, Event-Based Design and Run-time Verification of Composite Service Transactional Behavior, IEEE Transactions on Services Computing, vol. 3, no. 1, January-March 2010, 32–45

    Google Scholar 

  64. Iman Saleh, Gergory Kulczycki, M. Brian Blake, Yi Wei; Formal Methods for Data-Centric Web Services: From Model to Implementation; Proc. of IEEE 20th International Conference on Web Services, 2013, pp. 332–339

    Google Scholar 

  65. Jia Mei, Huaikou Miao, Qingguo Xu, Pan Liu; Modelling and Verifying Web Service Applications with Time Constraints; Proc. 9th IEEE/ACIS International Conference on Computer and Information Science, 2010, 791–795

    Google Scholar 

  66. Dimitris Dranidis, Ervin Ramollari, Dimitrios Kourtesis; Run-time Verification of Behavioural Conformance for Conversational Web Services; IEEE European Conference on Web Services Proc. of Seventh IEEE European Conference on Webservices, 2009, 139–147

    Google Scholar 

  67. Nawal Guermouche, Silvano Dal Zilio; Towards Timed Requirement Verification for Service Choreographies; 8th International Conference Conference on Collaborative Computing: Networking, Applications and Worksharing, Collaboratecom 2012 Pittsburgh, PA, United States, October 14–17, 2012, 117–126

    Google Scholar 

  68. Manman Chen, Tian Huat Tan, Jun Sun, Yang Liu, Jun Pang, and **aohong Li; Verification of Functional and Non-functional Requirements of Web Service Composition; LNCS 8144, 2013, 313–328

    Google Scholar 

  69. YuYu Yin, JianWei Yin, Ying Li, ShuiGuang Deng; Verifying Consistency of Web Services Using Type Theory; Proc. of IEEE Asia-Pacific Services Computing Conference, 2008, 1560–1567

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Teradata (R&D) India Pvt Ltd, Hyderabad, India

    Deepak Chenthati

  2. Kalinga Institute of Industrial Technology, Deemed to be University, Bhubaneswar, 751024, India

    Hrushikesha Mohanty

  3. School of Computer & Information Sciences (On leave), University of Hyderabad, Hyderabad, India

    Hrushikesha Mohanty

Authors
  1. Deepak Chenthati
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hrushikesha Mohanty
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Deepak Chenthati .

Editor information

Editors and Affiliations

  1. School of Computer and Information Sciences, University of Hyderabad, Hyderabad, Telangana, India

    Hrushikesha Mohanty

  2. School of Computer Engineering, KIIT University, Bhubaneswar, Odisha, India

    Prasant Kumar Pattnaik

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Singapore Pte Ltd.

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Chenthati, D., Mohanty, H. (2019). Service Modelling and Verification: A Formal Approach. In: Mohanty, H., Pattnaik, P. (eds) Webservices. Springer, Singapore. https://doi.org/10.1007/978-981-13-3224-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-981-13-3224-1_1

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-13-3223-4

  • Online ISBN: 978-981-13-3224-1

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation