An Experimentation Framework for Specification and Verification of Web Services
Szymon Katra, Wiktor Daszczuk, Danny Czejdo
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 913–917 (2022)
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.
References
- 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
- 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
- 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
- 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
- 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
- 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
- R. Milner, A Calculus of Communicating Systems, LNCS vol. 92, vol. 92. Berlin, Heidelberg: Springer Berlin Heidelberg, 1980. ISBN 978-3-540-10235-9
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- E. Christensen, F. Curbera, G. Meredith, and S. Weerawarana, “Web Services Description Language (WSDL),” 2001. https://www.w3.org/TR/wsdl.html
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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.