{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T08:10:02Z","timestamp":1746259802852,"version":"3.40.4"},"reference-count":29,"publisher":"IGI Global","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,10,1]]},"abstract":"<p>In this paper, we propose a bounded model-checking based approach for the verification of declarative Web services composition processes using satisfiability solving (SAT). The need for the bounded model-checking approach stems from the nature of declarative processes as they are defined by only specifying the constraints that mark the boundary of the solution to the composition process. The proposed approach relies on using Event Calculus (EC) as the modeling formalism with a sound and complete EC to SAT encoding process. The use of EC as the modeling also formalism allows for a highly expressive approach for both the specification of composition model and for the specification of verification properties. Furthermore, as the conflict clauses returned by the SAT solver can be significantly large for complex processes and verification requirements, we propose a filtering criterion and defined patterns for identifying the clauses of interest for process verification.<\/p>","DOI":"10.4018\/ijwsr.2013100103","type":"journal-article","created":{"date-parts":[[2014,6,6]],"date-time":"2014-06-06T14:07:36Z","timestamp":1402063656000},"page":"62-81","source":"Crossref","is-referenced-by-count":5,"title":["A Bounded Model Checking Approach for the Verification of Web Services Composition"],"prefix":"10.4018","volume":"10","author":[{"given":"Ehtesham","family":"Zahoor","sequence":"first","affiliation":[{"name":"National University of Computer and Emerging Sciences, Islamabad, Pakistan"}]},{"given":"Kashif","family":"Munir","sequence":"additional","affiliation":[{"name":"National University of Computer and Emerging Sciences, Islamabad, Pakistan"}]},{"given":"Olivier","family":"Perrin","sequence":"additional","affiliation":[{"name":"Laboratoire Lorrain de Recherche en Informatique et Ses Applications (LORIA), Universit\u00e9 de Lorraine, Lorraine, France"}]},{"given":"Claude","family":"Godart","sequence":"additional","affiliation":[{"name":"Laboratoire Lorrain de Recherche en Informatique et Ses Applications (LORIA), Universit\u00e9 de Lorraine, Lorraine, France"}]}],"member":"2432","reference":[{"key":"ijwsr.2013100103-0","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31811-8_2"},{"key":"ijwsr.2013100103-1","doi-asserted-by":"publisher","DOI":"10.1007\/11549970_17"},{"key":"ijwsr.2013100103-2","doi-asserted-by":"crossref","unstructured":"Dijkman, R. M., Dumas, M., & Ouyang, C. (2007). Formal semantics and analysis of BPMN process models.","DOI":"10.1016\/j.infsof.2008.02.006"},{"key":"ijwsr.2013100103-3","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_13"},{"key":"ijwsr.2013100103-4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56863-8_36"},{"key":"ijwsr.2013100103-5","doi-asserted-by":"crossref","unstructured":"Ferrara, A. (2004, November). Web services: A process algebra approach. In Proceedings of the 2nd International Conference on Service Oriented Computing (pp. 242-251). ACM.","DOI":"10.1145\/1035167.1035202"},{"key":"ijwsr.2013100103-6","doi-asserted-by":"crossref","unstructured":"Fu, X., Bultan, T., & Su, J. (2004, May). Analysis of interacting BPEL web services. In Proceedings of the 13th International Conference on World Wide Web (pp. 621-630). ACM.","DOI":"10.1145\/988672.988756"},{"key":"ijwsr.2013100103-7","unstructured":"Goedertier, S. (2008). Declarative techniques for modeling and mining business processes."},{"key":"ijwsr.2013100103-8","doi-asserted-by":"crossref","unstructured":"Guermouche, N., & Godart, C. (2009, July). Timed model checking based approach for web services analysis. In Proceedings of the IEEE International Conference on Web Services (ICWS 2009) (pp. 213-221). IEEE.","DOI":"10.1109\/ICWS.2009.42"},{"key":"ijwsr.2013100103-9","unstructured":"Hamadi, R., & Benatallah, B. (2003, January). A Petri net-based model for web service composition. In Proceedings of the 14th Australasian Database Conference (Vol. 17, pp. 191-200). Australian Computer Society, Inc."},{"key":"ijwsr.2013100103-10","doi-asserted-by":"publisher","DOI":"10.1007\/11538394_15"},{"key":"ijwsr.2013100103-11","unstructured":"Holzmann, G., & Checker, S. M. (2004). The primer and reference manual."},{"key":"ijwsr.2013100103-12","doi-asserted-by":"crossref","unstructured":"Hopcroft, J. E., Motwani, R., & Ullman, J. D. (2001). Introduction to automata theory, languages, and computation, 2nd.","DOI":"10.1145\/568438.568455"},{"key":"ijwsr.2013100103-13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45594-9_1"},{"key":"ijwsr.2013100103-14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83397-7_2"},{"key":"ijwsr.2013100103-15","unstructured":"Merz, M., Moldt, D., M\u00fcller, K., & Lamersdorf, W. (1995). Workflow modelling and execution with coloured Petri nets in COSM."},{"key":"ijwsr.2013100103-16","doi-asserted-by":"crossref","unstructured":"Morimoto, S. (2008). A survey of formal verification for business process modeling. In Proceedings of the Conference on Computational Science (ICCS 2008) (pp. 514-522). Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-540-69387-1_58"},{"key":"ijwsr.2013100103-17","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.5.703"},{"journal-title":"Commonsense reasoning","year":"2010","author":"E. T.Mueller","key":"ijwsr.2013100103-18"},{"key":"ijwsr.2013100103-19","doi-asserted-by":"crossref","unstructured":"Narayanan, S., & McIlraith, S. A. (2002, May). Simulation, verification and automated composition of web services. In Proceedings of the 11th International Conference on World Wide Web (pp. 77-88). ACM.","DOI":"10.1145\/511446.511457"},{"key":"ijwsr.2013100103-20","doi-asserted-by":"publisher","DOI":"10.1007\/s12599-009-0074-z"},{"key":"ijwsr.2013100103-21","doi-asserted-by":"publisher","DOI":"10.1504\/IJBPIM.2006.010025"},{"key":"ijwsr.2013100103-22","first-page":"1","author":"W. M.Van Der Aalst","year":"2006","journal-title":"DecSerFlow: Towards a truly declarative service flow language"},{"journal-title":"An introduction to modular process nets","year":"1996","author":"D.Wikarski","key":"ijwsr.2013100103-23"},{"key":"ijwsr.2013100103-24","doi-asserted-by":"crossref","unstructured":"Yi, X., & Kochut, K. J. (2004, July). A cp-nets-based design and verification framework for web services composition. In Proceedings of the IEEE International Conference on Web Services (pp. 756-760). IEEE.","DOI":"10.1109\/ICWS.2004.1314810"},{"key":"ijwsr.2013100103-25","unstructured":"Zahoor, E. (2011). Gouvernance de service: Aspects s\u00e9curit\u00e9 et donn\u00e9es (Doctoral dissertation, Universit\u00e9 Nancy II)."},{"key":"ijwsr.2013100103-26","doi-asserted-by":"crossref","unstructured":"Zahoor, E., Perrin, O., & Godart, C. (2010, July). Disc: A declarative framework for self-healing web services composition. In Proceedings of the 2010 IEEE International Conference on Web Services (ICWS) (pp. 25-33). IEEE.","DOI":"10.1109\/ICWS.2010.70"},{"key":"ijwsr.2013100103-27","doi-asserted-by":"crossref","unstructured":"Zahoor, E., Perrin, O., & Godart, C. (2010, December). Disc-set: Handling temporal and security aspects in the web services composition. In Proceedings of the 2010 IEEE 8th European Conference on Web Services (ECOWS) (pp. 51-58). IEEE.","DOI":"10.1109\/ECOWS.2010.18"},{"key":"ijwsr.2013100103-28","doi-asserted-by":"crossref","unstructured":"Zhang, J., Chang, C. K., Chung, J. Y., & Kim, S. W. (2004, July). WS-Net: A Petri-net based specification model for Web services. In Proceedings of the IEEE International Conference on Web Services (pp. 420-427). IEEE.","DOI":"10.1109\/ICWS.2004.1314766"}],"container-title":["International Journal of Web Services Research"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=108882","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T07:39:51Z","timestamp":1746257991000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/ijwsr.2013100103"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2013,10,1]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,10]]}},"URL":"https:\/\/doi.org\/10.4018\/ijwsr.2013100103","relation":{},"ISSN":["1545-7362","1546-5004"],"issn-type":[{"type":"print","value":"1545-7362"},{"type":"electronic","value":"1546-5004"}],"subject":[],"published":{"date-parts":[[2013,10,1]]}}}