{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:38Z","timestamp":1761611138199,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2004,9,1]],"date-time":"2004-09-01T00:00:00Z","timestamp":1093996800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2004,9]]},"abstract":"<jats:p>Verification techniques like model checking, preorder checking and equivalence checking are shown to be relevant to web service orchestration. The Concurrency Workbench of the New Century (CWB) is a verification tool that supports these verification techniques. By means of the Process Algebra Compiler (PAC), the CWB is modified to support the BPE-calculus. The BPE-calculus is a small language, based on BPEL4WS, to express web service orchestration. Both the syntax and the semantics of the BPE-calculus are formally defined. These are subsequently used as input for the PAC. As output, the PAC produces modules that are incorporated into the CWB so that it supports the BPE-calculus and, hence, provides a verification tool for web service orchestration.<\/jats:p>","DOI":"10.1145\/1022494.1022526","type":"journal-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:39:09Z","timestamp":1097170749000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":44,"title":["Modelling and verifying web service orchestration by means of the concurrency workbench"],"prefix":"10.1145","volume":"29","author":[{"given":"Mariya","family":"Koshkina","sequence":"first","affiliation":[{"name":"IBM, Markham, Canada"}]},{"given":"Franck","family":"van Breugel","sequence":"additional","affiliation":[{"name":"York University, Toronto, Canada"}]}],"member":"320","published-online":{"date-parts":[[2004,9]]},"reference":[{"key":"e_1_2_1_1_1","series-title":"Lecture Notes in Computer Science","first-page":"407","volume-title":"Proceedings of the 18th International Conference on Applications and Theory in Petri Nets","author":"van der Aalst W. M. P.","year":"1997"},{"key":"e_1_2_1_2_1","first-page":"174","article-title":"Challenges in business process management: Verification of business processes using Petri nets","volume":"80","author":"van der Aalst W. M. P.","year":"2003","journal-title":"Bulletin of the EATCS"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/7301.001.0001","volume-title":"van Hee. Workflow Management: Models, Methods, and Systems","author":"van der Aalst W. M. P.","year":"2002"},{"key":"e_1_2_1_4_1","series-title":"DAIMI PB series","first-page":"1","volume-title":"Proceedings of the Fourth Workshop on the Practical Use of Coloured Petri Nets and CPN Tools","author":"van der Aalst W. M. P.","year":"2002"},{"volume-title":"May","year":"2003","author":"Andrews T.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018982020561"},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/978-3-540-39958-2_9","volume-title":"Proceedings of the 6th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems","author":"Bocchi L.","year":"2003"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/820264.820459"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.414.0743"},{"volume-title":"March","year":"2001","author":"Christensen E.","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"volume-title":"Model Checking","year":"1999","author":"Clarke E. M.","key":"e_1_2_1_13_1"},{"volume-title":"July","year":"2000","author":"Cleaveland R.","key":"e_1_2_1_14_1"},{"issue":"2","key":"e_1_2_1_15_1","first-page":"50","article-title":"Modeling and verifying distributed systems using priorities: a case study","volume":"17","author":"Cleaveland R.","year":"1996","journal-title":"Software Concepts Tools"},{"key":"e_1_2_1_16_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/3-540-61474-5_87","volume-title":"Proceedings of the 8th Conference on Computer-Aided Verification","author":"Cleaveland R.","year":"1996"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(01)00033-8"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00031-7"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2003.1240303"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/988672.988756"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.06.010"},{"key":"e_1_2_1_22_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification","author":"Graf S.","year":"1997"},{"volume-title":"The Spin Model Checker: Primer and Reference Manual","year":"2003","author":"Holzmann G. J.","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2003.12.007"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/645343.650326"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/645345.650185"},{"volume-title":"York University","year":"2003","author":"Koshkina M.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"volume-title":"May","year":"2001","author":"Leymann F.","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.332.0326"},{"volume-title":"Concurrency: State Models and Java Programs","year":"1999","author":"Magee J.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","unstructured":"A. Martens. Distributed Business Processes --- Modeling and Verification by help of Web Services. PhD thesis Humboldt-Universit\u00e4t zu Berlin July 2003. Available at www.informatik.hu-berlin.de\/top\/download\/documents\/pdf\/Mar03.pdf. A. Martens. Distributed Business Processes --- Modeling and Verification by help of Web Services. PhD thesis Humboldt-Universit\u00e4t zu Berlin July 2003. Available at www.informatik.hu-berlin.de\/top\/download\/documents\/pdf\/Mar03.pdf."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/944217.944236"},{"key":"e_1_2_1_34_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"Milner R.","year":"1980"},{"volume-title":"Communication and Concurrency","year":"1989","author":"Milner R.","key":"e_1_2_1_35_1"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/580055.829303"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/794192.794873"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/511446.511457"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"e_1_2_1_40_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Proceedings of 5th GI-Conference on Theoretical Computer Science","author":"Park D.","year":"1981"},{"key":"e_1_2_1_41_1","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"W. M. P. van der Aalst, A. H. M. ter Hofstede, and M","author":"Piccinelli G.","year":"2003"},{"volume-title":"A structural approach to operational semantics. Report DAIMI FN-19","year":"1981","author":"Plotkin G. D.","key":"e_1_2_1_42_1"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/646673.699325"},{"volume-title":"November","year":"1999","author":"Sims S.","key":"e_1_2_1_44_1"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1022494.1022526","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1022494.1022526","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:30:57Z","timestamp":1750264257000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1022494.1022526"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,9]]},"references-count":44,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2004,9]]}},"alternative-id":["10.1145\/1022494.1022526"],"URL":"https:\/\/doi.org\/10.1145\/1022494.1022526","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2004,9]]},"assertion":[{"value":"2004-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}