{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T17:20:59Z","timestamp":1743009659258,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319246253"},{"type":"electronic","value":"9783319246260"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24626-0_13","type":"book-chapter","created":{"date-parts":[[2015,10,13]],"date-time":"2015-10-13T07:02:21Z","timestamp":1444719741000},"page":"171-186","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Model Checking Web Services Choreography"],"prefix":"10.1007","author":[{"given":"Arbia","family":"Ben Azaiez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zohra","family":"Sba\u00ef","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,25]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-63139-9_48","volume-title":"Application and Theory of Petri Nets 1997","author":"WMP Aalst van der","year":"1997","unstructured":"van der Aalst, W.M.P.: Verification of workflow nets. In: Az\u00e9ma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 407\u2013426. Springer, Heidelberg (1997)"},{"key":"13_CR3","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218126698000043","volume":"8","author":"W Aalst van der","year":"1998","unstructured":"van der Aalst, W.: The application of petri nets to workflow management. J. Circuits Syst. Comput. 8, 21\u201366 (1998)","journal-title":"J. Circuits Syst. Comput."},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.entcs.2006.04.004","volume":"158","author":"A Antonik","year":"2006","unstructured":"Antonik, A., Huth, M.: Efficient patterns for model checking partial state spaces in CTL intersection LTL. Electr. Notes Theor. Comput. Sci. 158, 41\u201357 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"13_CR5","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)"},{"issue":"1","key":"13_CR6","first-page":"51","volume":"5","author":"K Barkaoui","year":"2007","unstructured":"Barkaoui, K., Ben Ayed, R., Sba\u00ef, Z.: Workflow soundness verification based on structure theory of petri nets. Int. J. Comput. Inf. Sci. (IJCIS) 5(1), 51\u201361 (2007)","journal-title":"Int. J. Comput. Inf. Sci. (IJCIS)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-20633-7_30","volume-title":"Service-Oriented Perspectives in Design Science Research","author":"E Caliz","year":"2011","unstructured":"Caliz, E., Umapathy, K., S\u00e1nchez-Ru\u00edz, A.J., Elfayoumy, S.A.: Analyzing web service choreography specifications using colored petri nets. In: Jain, H., Sinha, A.P., Vitharana, P. (eds.) DESRIST 2011. LNCS, vol. 6629, pp. 412\u2013426. Springer, Heidelberg (2011)"},{"issue":"4","key":"13_CR8","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transfer 2(4), 410\u2013425 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"13_CR9","unstructured":"Decker, G., Overdick, H., Zaha, J.M.: On the suitability of WS-CDL for choreography modeling. In: Proceedings of Methoden, Konzepte Und Technologien Fur Die Entwicklung Von Dienstebasierten Informationssystemen (EMISA 2006) (2006)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Diaz, G., Cambronero, M.E., Pardo, J.J., Valero, V., Cuartero, O.: Model checking techniques applied to the design of web services (2007)","DOI":"10.19153\/cleiej.10.2.2"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based analysis of obligations in web service choreography. In: International Conference on Internet and Web Applications and Services (AICT-ICIW 2006), IEEE Computer Society (2006)","DOI":"10.1109\/AICT-ICIW.2006.131"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/978-3-642-16901-4_38","volume-title":"Formal Methods and Software Engineering","author":"M Frappier","year":"2010","unstructured":"Frappier, M., Fraikin, B., Chossart, R., Chane-Yack-Fa, R., Ouenzar, M.: Comparison of model checking tools for information systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 581\u2013596. Springer, Heidelberg (2010)"},{"key":"13_CR13","unstructured":"Guerfel, R., Sba\u00ef, Z.: D&A4WSC as a design and analysis framework of web services composition. In: Proceedings of the International Workshop on Petri Nets and Software Engineering (PNSE 2014), in conjunction with Petri nets and ACSD, pp. 337\u2013338 (2014)"},{"key":"13_CR14","first-page":"140","volume":"2","author":"R Guerfel","year":"2013","unstructured":"Guerfel, R., Sba\u00ef, Z., Barkaoui, K.: Modeling and formal verification framework of web services composition. Int. Conf. Control Eng. Inf. Technol. (CEIT 2013) 2, 140\u2013145 (2013)","journal-title":"Int. Conf. Control Eng. Inf. Technol. (CEIT 2013)"},{"issue":"2","key":"13_CR15","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T Henzinger","year":"1994","unstructured":"Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193\u2013244 (1994)","journal-title":"Inf. Comput."},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Hongli, Y., Xiangpeng, Z., Zongyan, Q., Geguang, P., Shuling, W.: A formal model of web service choreography description language(WS-CDL. Technical report) (2006)","DOI":"10.1007\/11841197_18"},{"key":"13_CR17","first-page":"35","volume":"1","author":"P Massuthe","year":"2005","unstructured":"Massuthe, P., Reisig, W., Schmidt, K.: An operating guideline approach to the SOA. Ann. Math. Comput. Teleinformatics 1, 35\u201343 (2005)","journal-title":"Ann. Math. Comput. Teleinformatics"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Pu, G., Shi, J., Wang, Z., Jin, L., Liu, J., He, J.: The validation and verification of WSCDL. In: Asia-Pacific Software Engineering Conference. IEEE, Los Alamitos. pp. 81\u201388 (2007)","DOI":"10.1109\/ASPEC.2007.79"},{"issue":"5","key":"13_CR19","first-page":"33","volume":"18","author":"Z Sba\u00ef","year":"2013","unstructured":"Sba\u00ef, Z., Barkaoui, K.: V\u00e9rification formelle des processus workflow - extension aux workflows inter-organisationnels. Revue Ingnierie des Systmes d\u2019Information (ISI) 18(5), 33\u201357 (2013)","journal-title":"Revue Ingnierie des Systmes d\u2019Information (ISI)"},{"key":"13_CR20","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-662-44860-1_10","volume-title":"Enterprise and Organizational Modeling and Simulation","author":"Z Sba\u00ef","year":"2014","unstructured":"Sba\u00ef, Z., Barkaoui, K.: On compatibility analysis of inter organizational business processes. In: Barjis, J., Pergl, R. (eds.) EOMAS 2014. LNBIP, vol. 191, pp. 171\u2013186. Springer, Heidelberg (2014)"},{"key":"13_CR21","unstructured":"Xiangpeng, Z., Hongli, Y., Chao, C., Xiwu, D., Zongyan, Q.: Verification of WS-CDL choreography. In: Asian Working Conference on Verified Software. UNU-IIST, Macao SAR, China (2006)"}],"container-title":["Lecture Notes in Business Information Processing","Enterprise and Organizational Modeling and Simulation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24626-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:29:17Z","timestamp":1559266157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24626-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319246253","9783319246260"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24626-0_13","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"type":"print","value":"1865-1348"},{"type":"electronic","value":"1865-1356"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}