{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:59:57Z","timestamp":1742389197669},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540792291"},{"type":"electronic","value":"9783540792307"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79230-7_3","type":"book-chapter","created":{"date-parts":[[2008,4,12]],"date-time":"2008-04-12T06:53:23Z","timestamp":1207983203000},"page":"31-45","source":"Crossref","is-referenced-by-count":3,"title":["Extending Model Checking to Data-Aware Temporal Properties of Web Services"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Hall\u00e9","sequence":"first","affiliation":[]},{"given":"Roger","family":"Villemaire","sequence":"additional","affiliation":[]},{"given":"Omar","family":"Cherkaoui","sequence":"additional","affiliation":[]},{"given":"J\u00e9r\u00f4me","family":"Tremblay","sequence":"additional","affiliation":[]},{"given":"Boubker","family":"Ghandour","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"The Edinburgh concurrency workbench"},{"key":"3_CR2","volume-title":"Web Services, Concepts, Architectures and Applications","author":"G. Alonso","year":"2004","unstructured":"Alonso, G., Casati, F., Kuno, H., Machiraju, V.: Web Services, Concepts, Architectures and Applications. Springer, Heidelberg (2004)"},{"issue":"1","key":"3_CR3","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM\u00a041(1), 181\u2013204 (1994)","journal-title":"J. ACM"},{"key":"3_CR4","doi-asserted-by":"publisher","first-page":"826","DOI":"10.1145\/1066677.1066866","volume-title":"SAC","author":"J. Arias-Fisteus","year":"2005","unstructured":"Arias-Fisteus, J., Fern\u00e1ndez, L.S., Kloos, C.D.: Applying model checking to BPEL4WS business collaborations. In: Haddad, H., Liebrock, L.M., Omicini, A., Wainwright, R.L. (eds.) SAC, pp. 826\u2013830. ACM, New York (2005)"},{"key":"3_CR5","unstructured":"Berardi, D., Calvanese, D., De Giacomo, G., Hull, R., Mecella, M.: Automatic composition of transition-based semantic web services with messaging. In: B\u00f6hm,, et al. (eds.) [6], pp. 613\u2013624"},{"key":"3_CR6","unstructured":"B\u00f6hm, K., Jensen, C.S., Haas, L.M., Kersten, M.L., Larson, P.-\u00c5., Ooi, B.C. (eds.): Proceedings of the 31st International Conference on Very Large Data Bases, Trondheim, Norway, August 30 - September 2, 2005. ACM, New York (2005)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Web Services and Formal Methods","year":"2006","unstructured":"Bravetti, M., N\u00fa\u00f1ez, M., Zavattaro, G. (eds.): WS-FM 2006. LNCS, vol.\u00a04184. Springer, Heidelberg (2006)"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/j.entcs.2004.05.007","volume":"105","author":"A. Brogi","year":"2004","unstructured":"Brogi, A., Canal, C., Pimentel, E., Vallecillo, A.: Formalizing web service choreographies. Electr. Notes Theor. Comput. Sci.\u00a0105, 73\u201394 (2004)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Bultan, T., Fu, X., Hull, R., Su, J.: Conversation specification: a new approach to design and analysis of e-service composition. In: WWW, pp. 403\u2013410 (2003)","DOI":"10.1145\/775152.775210"},{"key":"3_CR10","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.M., 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.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"3_CR11","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Decker, G., Zaha, J.M., Dumas, M.: Execution semantics for service choreographies. In: Bravetti, et al. (eds.) [7], pp. 163\u2013177","DOI":"10.1007\/11841197_11"},{"key":"3_CR13","first-page":"113","volume-title":"TIME","author":"S. Demri","year":"2005","unstructured":"Demri, S., Lazic, R., Nowak, D.: On the freeze quantifier in constraint LTL: Decidability and complexity. In: TIME, pp. 113\u2013121. IEEE Computer Society, Los Alamitos (2005)"},{"key":"3_CR14","first-page":"71","volume-title":"PODS","author":"A. Deutsch","year":"2004","unstructured":"Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web services. In: Deutsch, A. (ed.) PODS, pp. 71\u201382. ACM, New York (2004)"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1145\/1035167.1035201","volume-title":"ICSOC","author":"Z. Duan","year":"2004","unstructured":"Duan, Z., Bernstein, A.J., Lewis, P.M., Lu, S.: A model for abstract process specification, verification and composition. In: Aiello, M., Aoyama, M., Curbera, F., Papazoglou, M.P. (eds.) ICSOC, pp. 232\u2013241. ACM, New York (2004)"},{"key":"3_CR16","first-page":"149","volume-title":"AICT\/ICIW","author":"H. Foster","year":"2006","unstructured":"Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based analysis of obligations in web service choreography. In: AICT\/ICIW, p. 149. IEEE Computer Society, Los Alamitos (2006)"},{"key":"3_CR17","unstructured":"Garey, M.R., Johnson, D.S.: Computers and intractability, a guide to the theory of NP-completeness. W. H. Freeman, San Francisco (1979)"},{"key":"3_CR18","unstructured":"Greenfield, P., Kuo, D., Nepal, S., Fekete, A.: Consistency for web services applications. In: B\u00f6hm, et al. (eds.) [6], pp. 1199\u20131203"},{"key":"3_CR19","first-page":"27","volume-title":"TIME","author":"S. Hall\u00e9","year":"2006","unstructured":"Hall\u00e9, S., Villemaire, R., Cherkaoui, O.: CTL model checking for labelled tree queries. In: TIME, pp. 27\u201335. IEEE Computer Society, Los Alamitos (2006)"},{"key":"3_CR20","first-page":"267","volume-title":"EDOC","author":"S. Hall\u00e9","year":"2007","unstructured":"Hall\u00e9, S., Villemaire, R., Cherkaoui, O., Ghandour, B.: Model-checking data-aware temporal workflow properties with CTL-FO+. In: EDOC, pp. 267\u2013278. IEEE Computer Society, Los Alamitos (2007)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/978-3-540-31984-9_4","volume-title":"Fundamental Approaches to Software Engineering","author":"R. Heckel","year":"2005","unstructured":"Heckel, R., Mariani, L.: Automatic conformance testing of web services. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol.\u00a03442, pp. 34\u201348. Springer, Heidelberg (2005)"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/11538394_15","volume-title":"Business Process Management","author":"S. Hinz","year":"2005","unstructured":"Hinz, S., Schmidt, K., Stahl, C.: Transforming BPEL to Petri nets. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol.\u00a03649, pp. 220\u2013235. Springer, Heidelberg (2005)"},{"key":"3_CR23","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)"},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/j.entcs.2004.02.022","volume":"105","author":"J.E. Johnson","year":"2004","unstructured":"Johnson, J.E., Langworthy, D.E., Lamport, L., Vogt, F.H.: Formal specification of a web services protocol. Electr. Notes Theor. Comput. Sci.\u00a0105, 147\u2013158 (2004)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR25","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1145\/1135777.1135819","volume-title":"WWW","author":"R. Kazhamiakin","year":"2006","unstructured":"Kazhamiakin, R., Pistore, M., Santuari, L.: Analysis of communication models in web service compositions. In: Carr, L., Roure, D.D., Iyengar, A., Goble, C.A., Dahlin, M. (eds.) WWW, pp. 267\u2013276. ACM, New York (2006)"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Koshkina, M., van Breugel, F.: Modelling and verifying web service orchestration by means of the concurrency workbench. ACM SIGSOFT SEN\u00a029(5) (September 2004)","DOI":"10.1145\/1022494.1022526"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/3-540-60045-0_60","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1995","unstructured":"Kupferman, O.: Augmenting branching temporal logics with existential quantification over atomic propositions. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 325\u2013338. Springer, Heidelberg (1995)"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11841760_3","volume-title":"Business Process Management","author":"N. Lohmann","year":"2006","unstructured":"Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing interacting BPEL processes. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol.\u00a04102, pp. 17\u201332. Springer, Heidelberg (2006)"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1007\/978-3-540-27834-4_60","volume-title":"Web Engineering","author":"S. Nakajima","year":"2004","unstructured":"Nakajima, S.: Model-checking of safety and security aspects in web service flows. In: Koch, N., Fraternali, P., Wirsing, M. (eds.) ICWE 2004. LNCS, vol.\u00a03140, pp. 488\u2013501. Springer, Heidelberg (2004)"},{"key":"3_CR30","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.entcs.2004.05.005","volume":"105","author":"M. Pistore","year":"2004","unstructured":"Pistore, M., Roveri, M., Busetta, P.: Requirements-driven verification of web services. Electr. Notes Theor. Comput. Sci.\u00a0105, 95\u2013108 (2004)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/11817949_8","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"A. Rensink","year":"2006","unstructured":"Rensink, A.: Model checking quantified computation tree logic. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 110\u2013125. Springer, Heidelberg (2006)"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/11562436_34","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"K.J. Turner","year":"2005","unstructured":"Turner, K.J.: Formalising web services. In: Wang, F. (ed.) FORTE 2005. LNCS, vol.\u00a03731, pp. 473\u2013488. Springer, Heidelberg (2005)"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P., Pesic, M.: DecSerFlow: Towards a truly declarative service flow language. In: Bravetti, et al.(eds.) [7], pp. 1\u201323","DOI":"10.1007\/11841197_1"},{"key":"3_CR34","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.entcs.2004.05.004","volume":"105","author":"M. Venzke","year":"2004","unstructured":"Venzke, M.: Specifications using XQuery expressions on traces. Electr. Notes Theor. Comput. Sci.\u00a0105, 109\u2013118 (2004)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR35","first-page":"45","volume-title":"EDOC","author":"J.M. Zaha","year":"2006","unstructured":"Zaha, J.M., Dumas, M., ter Hofstede, A., Barros, A., Decker, G.: Service interaction modeling: Bridging global and local views. In: EDOC, pp. 45\u201355. IEEE Computer Society, Los Alamitos (2006)"}],"container-title":["Lecture Notes in Computer Science","Web Services and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79230-7_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:14:31Z","timestamp":1619522071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79230-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540792291","9783540792307"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79230-7_3","relation":{},"subject":[]}}