{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T16:40:17Z","timestamp":1718383217451},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2024,1,23]],"date-time":"2024-01-23T00:00:00Z","timestamp":1705968000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,23]],"date-time":"2024-01-23T00:00:00Z","timestamp":1705968000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Syst Assur Eng Manag"],"published-print":{"date-parts":[[2024,6]]},"DOI":"10.1007\/s13198-023-02246-y","type":"journal-article","created":{"date-parts":[[2024,1,23]],"date-time":"2024-01-23T05:21:41Z","timestamp":1705987301000},"page":"2312-2327","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verification of transaction-aware web services composition through formal methods"],"prefix":"10.1007","volume":"15","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-7279-5971","authenticated-orcid":false,"given":"Sunita","family":"Jalal","sequence":"first","affiliation":[]},{"given":"Chetan Singh","family":"Negi","sequence":"additional","affiliation":[]},{"given":"Dharmendra Kumar","family":"Yadav","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,1,23]]},"reference":[{"key":"2246_CR1","doi-asserted-by":"crossref","unstructured":"Abbassi I, Graiet M, Gaaloul W, Hadj-Alouane NB (2015) Genetic-based approach for ATS and SLA-aware web services composition. In: International conference on web information systems engineering, pp 369\u2013383","DOI":"10.1007\/978-3-319-26190-4_25"},{"key":"2246_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in event-B: system and software engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R (2010) Modeling in event-B: system and software engineering. Cambridge University Press, Cambridge"},{"issue":"2","key":"2246_CR3","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1016\/j.eswa.2012.07.069","volume":"40","author":"J Bentahar","year":"2013","unstructured":"Bentahar J, Yahyaoui H, Kova M, Maamar Z (2013) Symbolic model checking composite web services using operational and control behaviors. Expert Syst Appl 40(2):508\u2013522","journal-title":"Expert Syst Appl"},{"issue":"2","key":"2246_CR4","doi-asserted-by":"publisher","first-page":"64","DOI":"10.4018\/jdm.2011040103","volume":"22","author":"S Bhiri","year":"2011","unstructured":"Bhiri S, Gaaloul W, Godart C, Perrin O, Zaremba M, Derguech W (2011) Ensuring customised transactional reliability of composite services. J Database Manag 22(2):64\u201392","journal-title":"J Database Manag"},{"key":"2246_CR5","doi-asserted-by":"crossref","unstructured":"Bhiri S, Perrin O, Godart C (2005) Ensuring required failure atomicity of composite web services. In: Proceedings of the 14th international conference on world wide web, pp 138\u2013147","DOI":"10.1145\/1060745.1060769"},{"key":"2246_CR6","doi-asserted-by":"crossref","unstructured":"Boumlik L, Mejri M (2015) Toward the formalization of BPEL. In International conference on service-oriented computing, pp 157\u2013167","DOI":"10.1007\/978-3-662-50539-7_13"},{"key":"2246_CR7","doi-asserted-by":"crossref","unstructured":"Bourne S, Szabo C, Sheng QZ (2013) Verifying transactional requirements of web service compositions using temporal logic templates. In: International conference on web information systems engineering, pp 243\u2013256","DOI":"10.1007\/978-3-642-41230-1_21"},{"key":"2246_CR8","doi-asserted-by":"crossref","unstructured":"Bourne S, Szabo C, Sheng QZ (2015) Tl-views: a tool for temporal logic verification of transactional behavior of web service compositions. In: Service-oriented computing-icsoc 2014 workshops, pp 418\u2013422","DOI":"10.1007\/978-3-319-22885-3_39"},{"key":"2246_CR9","doi-asserted-by":"crossref","unstructured":"Browne MC, Clarke EM, Gr\u00fcmberg O (1987) Characterizing Kripke structures in temporal logic. In: Colloquium on trees in algebra and programming, pp 256\u2013270","DOI":"10.1007\/3-540-17660-8_60"},{"issue":"5","key":"2246_CR10","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/j.jlap.2008.09.002","volume":"78","author":"ME Cambronero","year":"2009","unstructured":"Cambronero ME, D\u0131 G, Maci\u00e0 H et al (2009) A petri net approach for the design and analysis of web services choreographies. J Logic Algebraic Program 78(5):359\u2013380","journal-title":"J Logic Algebraic Program"},{"key":"2246_CR11","doi-asserted-by":"crossref","unstructured":"Chaurasia BK, Keshari S, Verma S, Tomar G (2010) Verification of privacy preserving authentication protocol for VANETs. In: 2010 international conference on computational intelligence and communication networks, pp 243\u2013248","DOI":"10.1109\/CICN.2010.58"},{"issue":"2","key":"2246_CR12","first-page":"120","volume":"2","author":"BK Chaurasia","year":"2012","unstructured":"Chaurasia BK, Verma S (2012) Model-based verification of privacy preserving authentication protocol for VANETs. Int J Inf Technol Commun Converg 2(2):120\u2013137","journal-title":"Int J Inf Technol Commun Converg"},{"key":"2246_CR13","doi-asserted-by":"crossref","unstructured":"Ciancia, V, Ferrari GL, Guanciale R, Strollo D (2008) Checking correctness of transactional behaviors. In: International conference on formal techniques for networked and distributed systems, pp 134\u2013148","DOI":"10.1007\/978-3-540-68855-6_9"},{"key":"2246_CR14","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M , Roveri M, Tacchella A (2002) Nusmv 2: an opensource tool for symbolic model checking. In: International conference on computer aided verification, pp 359\u2013364","DOI":"10.1007\/3-540-45657-0_29"},{"key":"2246_CR15","doi-asserted-by":"crossref","unstructured":"Clarke EM, Draghicescu IA (1988) Expressibility results for linear-time and branching-time logics. In: Workshop\/school\/symposium of the rex project (research and education in concurrent systems), pp 428\u2013437","DOI":"10.1007\/BFb0013029"},{"key":"2246_CR16","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1016\/j.asoc.2015.11.012","volume":"39","author":"M Cremene","year":"2016","unstructured":"Cremene M, Suciu M, Pallez D, Dumitrescu D (2016) Comparative analysis of multi-objective evolutionary algorithms for QoS-aware web service composition. Appl Soft Comput 39:124\u2013139","journal-title":"Appl Soft Comput"},{"issue":"1","key":"2246_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1504\/IJWGS.2005.007545","volume":"1","author":"S Dustdar","year":"2005","unstructured":"Dustdar S, Schreiner W (2005) A survey on web services composition. Int J Web Grid Serv 1(1):1\u201330","journal-title":"Int J Web Grid Serv"},{"issue":"1","key":"2246_CR18","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1109\/TSC.2010.5","volume":"3","author":"J El Hadad","year":"2010","unstructured":"El Hadad J, Manouvrier M, Rukoz M (2010) Tqos: Transactional and QoS-aware selection algorithm for automatic web service composition. IEEE Trans Serv Comput 3(1):73\u201385","journal-title":"IEEE Trans Serv Comput"},{"key":"2246_CR19","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson T, Armstrong P, Boulgakov A, Roscoe AW (2014) Fdr3\u2013a modern refinement checker for CSP. In: International conference on tools and algorithms for the construction and analysis of systems, pp 187\u2013201","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"2246_CR20","doi-asserted-by":"publisher","DOI":"10.1016\/j.jocs.2020.101165","volume":"44","author":"Y Hammal","year":"2020","unstructured":"Hammal Y, Mansour KS, Abdelli A, Mokdad L (2020) Formal techniques for consistency checking of orchestrations of semantic web services. J Comput Sci. 44:101165","journal-title":"J Comput Sci."},{"issue":"8","key":"2246_CR21","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare CAR (1978) Communicating sequential processes. Commun ACM 21(8):666\u2013677","journal-title":"Commun ACM"},{"key":"2246_CR22","first-page":"2511","volume":"5","author":"A Imed","year":"2021","unstructured":"Imed A, Mammar A, Graiet M (2021) A correct-by-construction model for verifying transactional composite services configuration. IEEE Trans Serv Comput 5:2511\u20132525","journal-title":"IEEE Trans Serv Comput"},{"key":"2246_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/b95112","volume-title":"Coloured petri nets: modelling and validation of concurrent systems","author":"K Jensen","year":"2009","unstructured":"Jensen K, Kristensen LM (2009) Coloured petri nets: modelling and validation of concurrent systems. Springer, Berlin"},{"key":"2246_CR24","unstructured":"Jordan D, Evdemon J, Alves A, Arkin A, Askary S, Barreto C, et al (2007) Web services business process execution language version 2.0. OASIS standard. 11(120): 5"},{"issue":"2","key":"2246_CR25","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1109\/TSC.2015.2449850","volume":"10","author":"A Khaled","year":"2015","unstructured":"Khaled A, Miller J (2015) Using $$\\pi $$-calculus for formal modeling and verification of WS-CDL choreographies. IEEE Trans Serv Comput 10(2):316\u2013327","journal-title":"IEEE Trans Serv Comput"},{"key":"2246_CR26","doi-asserted-by":"crossref","unstructured":"Li J, Zhu H, He J (2008) Specifying and verifying web transactions. In: International conference on formal techniques for networked and distributed systems, pp 149\u2013168","DOI":"10.1007\/978-3-540-68855-6_10"},{"issue":"1","key":"2246_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1186\/s40064-015-0805-1","volume":"4","author":"D Nagamouttou","year":"2015","unstructured":"Nagamouttou D, Egambaram I, Krishnan M, Narasingam P (2015) A verification strategy for web services composition using enhanced stacked automata model. Springerplus 4(1):1\u201313","journal-title":"Springerplus"},{"issue":"2\u20133","key":"2246_CR28","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.scico.2007.03.002","volume":"67","author":"C Ouyang","year":"2007","unstructured":"Ouyang C, Verbeek E, Van Der Aalst WM, Breutel S, Dumas M, Ter Hofstede AH (2007) Formal semantics and analysis of control flow in WS-BPEL. Sci Comput Program 67(2\u20133):162\u2013198","journal-title":"Sci Comput Program"},{"key":"2246_CR29","unstructured":"Petri, C. (1966) Communication with automata [Ph. D. dissertation]. Rome Air Development Center, Rome, NY"},{"issue":"2","key":"2246_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1734103.1734118","volume":"35","author":"SH Ripon","year":"2010","unstructured":"Ripon SH (2010) Process algebraic support for web service composition. ACM SIGSOFT Softw Eng Notes 35(2):1\u20137","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"2246_CR31","doi-asserted-by":"crossref","unstructured":"Souri A, Rahmani AM, Navimipour NJ, Rezaei R (2019) Formal modeling and verification of a service composition approach in the social customer relationship management system. Inf Technol People","DOI":"10.1108\/ITP-02-2018-0109"},{"issue":"1","key":"2246_CR32","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1109\/TASE.2008.916747","volume":"6","author":"W Tan","year":"2008","unstructured":"Tan W, Fan Y, Zhou M (2008) A petri net-based method for compatibility analysis and composition of web services in business process execution language. IEEE Trans Autom Sci Eng 6(1):94\u2013106","journal-title":"IEEE Trans Autom Sci Eng"},{"key":"2246_CR33","doi-asserted-by":"crossref","unstructured":"Taoufik SR, Tahar BM, Layth S, Mourad K (2017) Towards a formal approach for the verification of SCA\/BPEL software architectures. In: 2017 8th international conference on information, intelligence, systems & applications (IISA), pp 1\u20136","DOI":"10.1109\/IISA.2017.8316371"},{"issue":"01","key":"2246_CR34","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218126698000043","volume":"8","author":"WM Van der Aalst","year":"1998","unstructured":"Van der Aalst WM (1998) The application of petri nets to workflow management. J Circuits Syst Comput 8(01):21\u201366","journal-title":"J Circuits Syst Comput"},{"key":"2246_CR35","unstructured":"Wan K, Kapoor HK, Das S, Raju B, Krilavi\u010dius T, Man KL (2012) Modelling and verification of compensating transactions using the spin tool. In: Engineers and computer scientists: 2012 IMECS: proceedings of the international multiconference, 2012, 14\u201316 March, 2012, Hong Kong, vol 2, pp 1163\u20131168"},{"issue":"5","key":"2246_CR36","doi-asserted-by":"publisher","first-page":"1112","DOI":"10.1016\/j.future.2012.12.010","volume":"29","author":"Q Wu","year":"2013","unstructured":"Wu Q, Zhu Q (2013) Transactional and QoS-aware dynamic service composition based on ant colony optimization. Futur Gener Comput Syst 29(5):1112\u20131119","journal-title":"Futur Gener Comput Syst"},{"issue":"1","key":"2246_CR37","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s11741-010-0109-3","volume":"14","author":"D Xu","year":"2010","unstructured":"Xu D, Lei Z, Li W-M, Zhang B-F (2010) Model checking web services choreography in process analysis toolkit. J Shanghai Univ (Engl Edn) 14(1):45\u201349","journal-title":"J Shanghai Univ (Engl Edn)"},{"issue":"1","key":"2246_CR38","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1177\/0037549707079227","volume":"83","author":"WL Yeung","year":"2007","unstructured":"Yeung WL (2007) CSP-based verification for web service orchestration and choreography. SIMULATION 83(1):65\u201374","journal-title":"SIMULATION"},{"issue":"10","key":"2246_CR39","doi-asserted-by":"publisher","first-page":"12772","DOI":"10.1016\/j.eswa.2011.04.068","volume":"38","author":"WL Yeung","year":"2011","unstructured":"Yeung WL (2011) A formal and visual modeling approach to choreography based web services composition and conformance verification. Expert Syst Appl 38(10):12772\u201312785","journal-title":"Expert Syst Appl"},{"key":"2246_CR40","doi-asserted-by":"crossref","unstructured":"Zatout S, Benabdelhafid MS, Boufaida M (2018) Formal transaction modeling and verification for an adaptable web service orchestration. In: 2018 IEEE international conference on software quality, reliability and security companion (QRS-C) (pp 531\u2013536)","DOI":"10.1109\/QRS-C.2018.00095"},{"issue":"5","key":"2246_CR41","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1002\/spe.2434","volume":"47","author":"Y Zhu","year":"2017","unstructured":"Zhu Y, Huang Z, Zhou H (2017) Modeling and verification of web services composition based on model transformation. Softw Pract Exp 47(5):709\u2013730","journal-title":"Softw Pract Exp"}],"container-title":["International Journal of System Assurance Engineering and Management"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13198-023-02246-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s13198-023-02246-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13198-023-02246-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T16:16:12Z","timestamp":1718381772000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s13198-023-02246-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,23]]},"references-count":41,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["2246"],"URL":"https:\/\/doi.org\/10.1007\/s13198-023-02246-y","relation":{},"ISSN":["0975-6809","0976-4348"],"issn-type":[{"value":"0975-6809","type":"print"},{"value":"0976-4348","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,23]]},"assertion":[{"value":"22 December 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 September 2023","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 December 2023","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 January 2024","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This article does not containing any studies involving human participants and animals.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Human Participants and\/or Animals:"}},{"value":"It does not apply to this article as no studies involve human participants.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Informed consent:"}}]}}
