Logo PTI Logo FedCSIS

Proceedings of the 17th Conference on Computer Science and Intelligence Systems

Annals of Computer Science and Information Systems, Volume 30

An Experimentation Framework for Specification and Verification of Web Services

, ,

DOI: http://dx.doi.org/10.15439/2022F188

Citation: Proceedings of the 17th Conference on Computer Science and Intelligence Systems, M. Ganzha, L. Maciaszek, M. Paprzycki, D. Ślęzak (eds). ACSIS, Vol. 30, pages 913917 ()

Full text

Abstract. Designing and implementing Web Services constitutes a large and constantly growing part of the information technology market. It requires efficient personnel training in the application's preparation (visual programming, libraries, repositories, code reusability) and other stages of development, such as formal verification. Web Services have specific scenarios in which distributed processes and network resources are used. This aspect of services requires integration with the model checkers. This article presents the experimentation framework in which services can be specified and then formally analyzed against deadlock-freedom, achievement of process goals, and similar features. This language enriches the basic Rybu language with the ability to use variables in processes, service calls between servers, new structural instructions, and other constructions known to programmers while remaining in line with declarative, mathematical IMDS formalism. Additionally, the development environment allows simulation of a counterexample or a witness - obtained as a result of the model checking - in a similar way to traditional debuggers.


  1. B. AL-Shargabi, A. El Sheikh, and A. Sabri, “Web Service Composition Survey: State of the Art Review,” Recent Patents Comput. Sci., vol. 3, no. 2, pp. 91–107, Jun. 2010. http://dx.doi.org/10.2174/2213275911003020091
  2. W. B. Daszczuk, “Specification and Verification in Integrated Model of Distributed Systems (IMDS),” MDPI Comput., vol. 7, no. 4, pp. 1–26, Dec. 2018. http://dx.doi.org/10.3390/computers7040065
  3. W. B. Daszczuk, “Using the Dedan Program,” in Integrated Model of Distributed Systems, Cham, Switzerland: Springer Nature, 2020, pp. 87–97. http://dx.doi.org/10.1007/978-3-030-12835-7_6
  4. W. B. Daszczuk, M. Bielecki, and J. Michalski, “Rybu: Imperative-style Preprocessor for Verification of Distributed Systems in the Dedan Environment,” in KKIO’17 – Software Engineering Conference, Rzeszów, Poland, 14-16 Sept. 2017, 2017, pp. 135–150. https://arxiv.org/abs/1710.02722
  5. M. Ghannoudi and W. Chainbi, “Formal verification for Web service composition: A model-checking approach,” in 2015 International Symposium on Networks, Computers and Communications (ISNCC), Yasmine Hammamet, Tunisia, 13-15 May 2015, 2015, pp. 1–6. http://dx.doi.org/10.1109/ISNCC.2015.7238576
  6. C. A. R. Hoare, “Communicating sequential processes,” Commun. ACM, vol. 21, no. 8, pp. 666–677, Aug. 1978. http://dx.doi.org/10.1145/359576.359585
  7. R. Milner, A Calculus of Communicating Systems, LNCS vol. 92, vol. 92. Berlin, Heidelberg: Springer Berlin Heidelberg, 1980. ISBN 978-3-540-10235-9
  8. H. Paik, A. L. Lemos, M. C. Barukh, B. Benatallah, and A. Natarajan, “Service Component Architecture (SCA),” in Web Service Implementation and Composition Techniques, Cham: Springer International Publishing, 2017, pp. 203–250. http://dx.doi.org/10.1007/978-3-319-55542-3_8
  9. W. Chargui, T. S. Rouis, M. Kmimech, M. T. Bhiri, L. Sliman, and B. Raddaoui, “Towards a formal verification approach for service component architecture,” in SOMET 2017: 16th International Conference on Intelligent Software Methodologies, Tools, and Techniques, Kitakyushu, Japan, 26-28 Sept 2017, 2017, pp. 466–479. http://dx.doi.org/10.3233/978-1-61499-800-6-466
  10. J. C. Corbett, M. B. Dwyer, and J. Hatcliff, “Bandera: a source-level interface for model checking Java programs,” in 22nd international conference on Software engineering - ICSE ’00, Limerick, Ireland, 4-11 June 2000, 2000, pp. 762–765. http://dx.doi.org/10.1145/337180.337625
  11. I. Bluemke, M. Kurek, and M. Purwin, “Tool for Automatic Testing of Web Services,” in 5th International Workshop Automating Test Case Design, Selection and Evaluation, FEDCSIS, Warsaw, Poland, 7–10 Sept 2014, 2014, pp. 1553–1558. http://dx.doi.org/10.15439/2014F93
  12. I. Bluemke and A. Sawicki, “Tool for Mutation Testing of Web Services,” in 13th DEPCOS/Reclomex, Brunów, Poland, 2-6 July 2018, 2019, pp. 46–55. http://dx.doi.org/10.1007/978-3-319-91446-6_5
  13. S. Ilieva, I. Manova, and D. Petrova-Antonova, “Towards a methodology for testing of business processes,” in 7th Federated Conference on Computer Science and Information Systems, FEDCSIS, Wroclaw, Poland, 09-12 Sept 2012, 2012, pp. 1315–1322. https://ieeexplore.ieee.org/document/6354354
  14. T. Preisler, T. Dethlefs, and W. Renz, “Simulation as a Service: A Design Approach for large-scale Energy Network Simulations,” in 10th Federated Conference on Computer Science and Information Systems, FedCSIS, Lodz, Poland, 13-16 Sept 2015, 2015, pp. 1765–1772. http://dx.doi.org/10.15439/2015F116
  15. G. R. Andrews et al., “An overview of the SR language and implementation,” ACM Trans. Program. Lang. Syst., vol. 10, no. 1, pp. 51–86, Jan. 1988. http://dx.doi.org/10.1145/42192.42324
  16. E. Christensen, F. Curbera, G. Meredith, and S. Weerawarana, “Web Services Description Language (WSDL),” 2001. https://www.w3.org/TR/wsdl.html
  17. L. Belava, “Concept of Platform for Hybrid Composition, Grounding and Execution of Web Services,” in 11th Conference on Advanced Information Technologies for Management, FEDCSIS, Kraków, Poland, 8–11 Sept 2013, 2013, pp. 1071 – 1077. https://annals-csis.org/Volume_1/pliks/190.pdf
  18. G. Baryannis and D. Plexousakis, “Automated Web Service Composition: State of the Art and Research Challenges,” 2010. https://publications.ics.forth.gr/tech-reports/2010/2010.TR409_Automated_Web_Service_Composition.pdf
  19. A. Niewiadomski, P. Switalski, M. Kowalczyk, and W. Penczek, “TripICS - a Web Service Composition System for Planning Trips and Travels,” Fundam. Informaticae, vol. 157, no. 4, pp. 403–425, Jan. 2018. http://dx.doi.org/10.3233/FI-2018-1635
  20. I. Pawełoszek, “Integrating Semantic Web Services into Financial Decision Support Process,” in 11th Conference on Advanced Information Technologies for Management, FEDCSIS, Gdansk, Poland, 11-14 Sept 2016, 2016, pp. 1189–1198. http://dx.doi.org/10.15439/2016F99
  21. S. De, P. Barnaghi, M. Bauer, and S. Meissner, “Service modelling for the Internet of Things,” in 6th Federated Conference on Computer Science and Information Systems, FedCSIS, Szczecin, Poland, 18-21 Sept 2011, 2011, pp. 949–955. https://ieeexplore.ieee.org/document/6078180
  22. S. Demirkol, M. Challenger, S. Getir, T. Kosar, G. Kardas, and M. Mernik, “SEA_L: A Domain-specific Language for Semantic Web enabled Multi-agent Systems,” in 7th Federated Conference on Computer Science and Information Systems, FEDCSIS, Wroclaw, Poland, 09-12 Sept 2012, 2012, pp. 1373–1380. https://ieeexplore.ieee.org/document/6354358
  23. W. B. Daszczuk, “Graphic modeling in Distributed Autonomous and Asynchronous Automata (DA3),” Softw. Syst. Model., vol. 20, no. 5, pp. 363–398, 2021. http://dx.doi.org/10.1007/s10270-021-00917-7
  24. S. Katra, “Specification and verification of Web Service composition in DedAn environment,” MSc thesis, Dept. of Electronics and Information Technology, Warsaw University of Technology, 2022.