{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:50:59Z","timestamp":1725749459256},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642412202"},{"type":"electronic","value":"9783642412219"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41221-9_1","type":"book-chapter","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T01:44:24Z","timestamp":1379900664000},"page":"1-33","source":"Crossref","is-referenced-by-count":4,"title":["Stepwise Development of Formal Models for Web Services Compositions: Modelling and Property Verification"],"prefix":"10.1007","author":[{"given":"Idir","family":"Ait-Sadoune","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yamine","family":"Ait-Ameur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-01918-0_2","volume-title":"Formal Methods for Web Services","author":"W.M.P. Aalst van der","year":"2009","unstructured":"van der Aalst, W.M.P., Mooij, A.J., Stahl, C., Wolf, K.: Service Interaction: Patterns, Formalization, and Analysis. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol.\u00a05569, pp. 42\u201388. Springer, Heidelberg (2009)"},{"key":"1_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press, New York (1996)"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"1_CR4","first-page":"1","volume":"77","author":"J.R. Abrial","year":"2007","unstructured":"Abrial, J.R., Hallerstede, S.: Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. Fundamenta Informaticae\u00a077, 1\u201328 (2007)","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"1_CR5","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10009-009-0109-2","volume":"11","author":"Y. Ait-Ameur","year":"2009","unstructured":"Ait-Ameur, Y., Baron, M., Kamel, N., Mota, J.M.: Encoding a process algebra using the Event B method. International Journal on Software Tools for Technology Transfer (STTT)\u00a011(3), 239\u2013253 (2009)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"1_CR6","series-title":"CCIS","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-88479-8_4","volume-title":"International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008)","author":"I. Ait-Sadoune","year":"2008","unstructured":"Ait-Sadoune, I., Ait-Ameur, Y.: Animating Event B Models by Formal Data Models. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol.\u00a017, pp. 37\u201355. Springer, Heidelberg (2008)"},{"key":"1_CR7","unstructured":"Ait-Sadoune, I., Ait-Ameur, Y.: From BPEL to Event-B. In: International Workshop on Integration of Model-based Methods and Tools at IFM Conference (2009)"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/ICECCS.2009.48","volume-title":"14th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)","author":"I. Ait-Sadoune","year":"2009","unstructured":"Ait-Sadoune, I., Ait-Ameur, Y.: A Proof Based Approach for Modelling and Verifying Web Services Compositions. In: 14th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 1\u201310. IEEE Computer Society, Potsdam (2009)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-642-11811-1_39","volume-title":"Abstract State Machines, Alloy, B and Z","author":"I. A\u00eft Sadoune","year":"2010","unstructured":"A\u00eft Sadoune, I., A\u00eft Ameur, Y.: A proof based approach for formal verification of transactional BPEL web services. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 405\u2013406. Springer, Heidelberg (2010)"},{"key":"1_CR10","series-title":"SCI","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-13273-5_4","volume-title":"Software Engineering Research, Management and Applications 2010","author":"I. Ait-Sadoune","year":"2010","unstructured":"Ait-Sadoune, I., Ait-Ameur, Y.: Stepwise Design of BPEL Web Services Compositions, An Event B Refinement Based Approach. In: Lee, R., Ormandjieva, O., Abran, A., Constantinides, C. (eds.) SERA 2010. SCI, vol.\u00a0296, pp. 51\u201368. Springer, Heidelberg (2010)"},{"issue":"5","key":"1_CR11","first-page":"1","volume":"1","author":"M.H. Beek ter","year":"2007","unstructured":"ter Beek, M.H., Bucchiarone, A., Gnesi, S.: Formal methods for service composition. Annals of Mathematics, Computing and Teleinformatics\u00a01(5), 1\u201310 (2007)","journal-title":"Annals of Mathematics, Computing and Teleinformatics"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-540-87603-8_3","volume-title":"Abstract State Machines, B and Z","author":"E. B\u00f6rger","year":"2008","unstructured":"B\u00f6rger, E., Thalheim, B.: Modeling Workflows, Interaction Patterns, Web Services and Business Processes: The ASM-Based Approach. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 24\u201338. Springer, Heidelberg (2008)"},{"key":"1_CR13","unstructured":"Brodt, R.: BPEL Designer Project (April 2012), \n                  \n                    http:\/\/www.eclipse.org\/bpel\/"},{"key":"1_CR14","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1977","unstructured":"Dijkstra, E.W.: A Discipline of Programming, 1st edn. Prentice Hall PTR, Upper Saddle River (1977)","edition":"1"},{"key":"1_CR15","unstructured":"Fahland, D., Reisig, W.: ASM-based semantics for BPEL: The negative Control Flow. In: 12th International Workshop on Abstract State Machines, pp. 131\u2013151 (2005)"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/11678564_13","volume-title":"Business Process Management Workshops","author":"R. Farahbod","year":"2006","unstructured":"Farahbod, R., Gl\u00e4sser, U., Vajihollahi, M.: An Abstract Machine Architecture for Web Service Based Business Process Management. In: Bussler, C.J., Haller, A. (eds.) BPM 2005 Workshops. LNCS, vol.\u00a03812, pp. 144\u2013157. Springer, Heidelberg (2006)"},{"key":"1_CR17","unstructured":"Foster, H.: A Rigorous Approach to Engineering Web Service Compositions. Ph.D. thesis, University of London (2006)"},{"key":"1_CR18","unstructured":"Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based Verification of Web Service Compositions. In: 18th IEEE International Conference on Automated Software Engineering (ASE 2003), pp. 152\u2013163 (2003)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Foster, H., Uchitel, S., Magee, J., Kramer, J.: LTSA-WS: A Tool for Model-Based Verification of Web Service Compositions and Choreography. In: 28th International Conference on Software Engineering, pp. 771\u2013774 (2006)","DOI":"10.1145\/1134285.1134408"},{"key":"1_CR20","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":"1_CR21","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. ACM\u00a012, 576\u2013580 (1969)","journal-title":"ACM"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-79230-7_6","volume-title":"Web Services and Formal Methods","author":"N. Lohmann","year":"2008","unstructured":"Lohmann, N.: A Feature-Complete Petri Net Semantics for WS-BPEL 2.0. In: Dumas, M., Heckel, R. (eds.) WS-FM 2007. LNCS, vol.\u00a04937, pp. 77\u201391. Springer, Heidelberg (2008)"},{"key":"1_CR23","unstructured":"Marconi, A.: Automated Process-level Composition of Web Services: from Requirements Specification to Process Run. Ph.D. thesis, University of Trento, Italy (2008)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-01918-0_3","volume-title":"Formal Methods for Web Services","author":"A. Marconi","year":"2009","unstructured":"Marconi, A., Pistore, M.: Synthesis and Composition of Web Services. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol.\u00a05569, pp. 89\u2013157. Springer, Heidelberg (2009)"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Nakajima, S.: Lightweight formal analysis of Web service flows. Progress in Informatics, 57\u201376 (2005)","DOI":"10.2201\/NiiPi.2005.2.5"},{"key":"1_CR26","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.entcs.2005.07.038","volume":"151","author":"S. Nakajima","year":"2006","unstructured":"Nakajima, S.: Model-Checking Behavioral Specification of BPEL Applications. Electronic Notes in Theoretical Computer Science\u00a0151, 89\u2013105 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"1_CR27","unstructured":"OASIS: Web Services Business Process Execution Language Version 2.0 (April 2007), \n                  \n                    http:\/\/bpel.xml.org\/"},{"key":"1_CR28","unstructured":"OMG: Business Process Model and Notation (BPMN) Version 2.0 (June 2010), \n                  \n                    http:\/\/www.omg.org\/spec\/BPMN\/2.0"},{"key":"1_CR29","unstructured":"Rodin: User Manual of the RODIN Platform (October 2007), \n                  \n                    http:\/\/deploy-eprints.ecs.soton.ac.uk\/11\/1\/manual-2.3.pdf"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Sala\u00fcn, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. In: IEEE International Conference on Web Services (ICWS 2004), pp. 43\u201351 (2004)","DOI":"10.1109\/ICWS.2004.1314722"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-540-30209-4_15","volume-title":"Web Services","author":"G. Sala\u00fcn","year":"2004","unstructured":"Sala\u00fcn, G., Ferrara, A., Chirichiello, A.: Negotiation Among Web Services Using LOTOS\/CADP. In: Zhang, L.-J., Jeckle, M. (eds.) ECOWS 2004. LNCS, vol.\u00a03250, pp. 198\u2013212. Springer, Heidelberg (2004)"},{"key":"1_CR32","unstructured":"Verbeek, H., van der Aalst, W.M.P: Analyzing BPEL processes using Petri nets. In: 2nd International Workshop on Applications of Petri Nets to Coordination, Workflow and Business Process Management (2005)"},{"key":"1_CR33","unstructured":"W3C: OWL-S: Semantic Markup for Web Services (November 2004), \n                  \n                    http:\/\/www.w3.org\/Submission\/OWL-S\/"},{"key":"1_CR34","unstructured":"W3C: Web Service Definition Language (WSDL 1.1) (February 2004), \n                  \n                    http:\/\/www.w3.org\/TR\/wsdl"},{"key":"1_CR35","unstructured":"W3C: Web Services Choreography Description Language Version 1.0 (November 2005), \n                  \n                    http:\/\/www.w3.org\/TR\/ws-cdl-10\/"},{"key":"1_CR36","unstructured":"WMC-WS: Process Definition Interface - XML Process Definition Language (October 2008), \n                  \n                    http:\/\/www.wfmc.org\/xpdl.html"}],"container-title":["Lecture Notes in Computer Science","Transactions on Large-Scale Data- and Knowledge-Centered Systems X"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41221-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T12:47:57Z","timestamp":1558097277000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41221-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642412202","9783642412219"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41221-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}