{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T18:50:20Z","timestamp":1771699820170,"version":"3.50.1"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T00:00:00Z","timestamp":1265846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2011,5]]},"DOI":"10.1007\/s10270-010-0149-9","type":"journal-article","created":{"date-parts":[[2010,2,10]],"date-time":"2010-02-10T06:52:55Z","timestamp":1265784775000},"page":"253-264","source":"Crossref","is-referenced-by-count":12,"title":["Verifying workflow processes: a transformation-based approach"],"prefix":"10.1007","volume":"10","author":[{"given":"Haiping","family":"Zha","sequence":"first","affiliation":[]},{"given":"Wil M. P.","family":"van der Aalst","sequence":"additional","affiliation":[]},{"given":"Jianmin","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Lijie","family":"Wen","sequence":"additional","affiliation":[]},{"given":"Jiaguang","family":"Sun","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,2,11]]},"reference":[{"key":"149_CR1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/7301.001.0001","volume-title":"Workflow Management: Models, Methods, and Systems","author":"W.M.P. Aalst van der","year":"2002","unstructured":"van der Aalst W.M.P., van Hee K.M.: Workflow Management: Models, Methods, and Systems. MIT Press, Cambridge (2002)"},{"issue":"1","key":"149_CR2","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/S0306-4379(00)00008-9","volume":"25","author":"W.M.P. Aalst van der","year":"2000","unstructured":"van der Aalst W.M.P., ter Hofstede A.H.M.: Verification of workflow task structures: a Petri-net-based approach. Inf. Syst. 25(1), 43\u201369 (2000)","journal-title":"Inf. Syst."},{"key":"149_CR3","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/S0169-023X(97)00032-3","volume":"362","author":"A.H.M. Hofstede ter","year":"1998","unstructured":"ter Hofstede A.H.M., Orlowska M.E., Rajapakse J.: Verification problems in conceptual workflow specifictions. Data Knowl. Eng. 362, 239\u2013256 (1998)","journal-title":"Data Knowl. Eng."},{"key":"149_CR4","unstructured":"DongFang Steam Turbine Works Co., Ltd. (2008) Home Page http:\/\/www.dfstw.com\/"},{"key":"149_CR5","doi-asserted-by":"crossref","unstructured":"Hinz, S., Schmidt, K., Stahl, C.: Transforming BPEL to Petri Nets. In: Proceedings of the BPM 2005. LNCS, vol. 3649, pp. 220\u2013235. Springer, Berlin (2005)","DOI":"10.1007\/11538394_15"},{"key":"149_CR6","doi-asserted-by":"crossref","unstructured":"van Dongen, B.F., van der Aalst, W.M.P., Verbeek, H.M.W.: Verification of EPCs: using reduction rule and Petri Nets. In: Proceedings of the CAiSE 2005. LNCS, vol. 3520, pp. 372\u2013386. Springer, Berlin (2005)","DOI":"10.1007\/11431855_26"},{"issue":"12","key":"149_CR7","doi-asserted-by":"crossref","first-page":"1281","DOI":"10.1016\/j.infsof.2008.02.006","volume":"50","author":"R.M. Dijkman","year":"2008","unstructured":"Dijkman R.M., Dumas M., Ouyang C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50(12), 1281\u20131294 (2008)","journal-title":"Inf. Softw. Technol."},{"key":"149_CR8","doi-asserted-by":"crossref","unstructured":"Zha, H., Yang, Y., Wang, J., Wen, L.: Transforming XPDL to Petri Nets. In: Proceedings of the BPM2007 Workshops. LNCS, vol. 4928, pp. 197\u2013207, Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78238-4_21"},{"issue":"1","key":"149_CR9","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1022883727209","volume":"14","author":"W.M.P. Aalst van der","year":"2003","unstructured":"van der Aalst W.M.P., Hofstede A.H.M., Kiepuszewski B., Barros A.P.: Workflow Patterns. Distrib. Parallel Databases 14(1), 5\u201351 (2003)","journal-title":"Distrib. Parallel Databases"},{"key":"149_CR10","unstructured":"TiPLM: Introduction to infotech product lifecycle management solution (in Chinese) (2008) http:\/\/www.thit.com.cn\/TiPLM\/TiPLM.htm"},{"issue":"4","key":"149_CR11","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1093\/comjnl\/44.4.246","volume":"44","author":"H.M.W. Verbeek","year":"2001","unstructured":"Verbeek H.M.W., Basten T., van der Aalst W.M.P.: Diagnosing workflow processes using woflan. Comput. J. 44(4), 246\u2013279 (2001)","journal-title":"Comput. J."},{"issue":"1","key":"149_CR12","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1142\/S0218126698000043","volume":"8","author":"W.M.P. Aalst van der","year":"1998","unstructured":"van der Aalst W.M.P.: The application of Petri nets to workflow management. J. Circuits Syst. Comput. 8(1), 21\u201366 (1998)","journal-title":"J. Circuits Syst. Comput."},{"key":"149_CR13","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T. Murata","year":"1989","unstructured":"Murata T.: Petri Nets: properties, analysis and applications. Proc. IEEE 77, 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"key":"149_CR14","doi-asserted-by":"crossref","first-page":"664","DOI":"10.1016\/S0377-2217(00)00292-7","volume":"134","author":"K. Salimifard","year":"2001","unstructured":"Salimifard K., Wright M.: Petri Net-based modeling of workflow systems: an overview. Eur. J. Oper. Res. 134, 664\u2013676 (2001)","journal-title":"Eur. J. Oper. Res."},{"key":"149_CR15","volume-title":"Patterns and XPDL: A Critical Evaluation of the XML Process Definition Language. QUT Technical report FIT-TR-2003-06","author":"W.M.P. Aalst","year":"2003","unstructured":"Aalst W.M.P.: Patterns and XPDL: A Critical Evaluation of the XML Process Definition Language. QUT Technical report FIT-TR-2003-06. Queensland University of Technology, Brisbane (2003)"},{"key":"149_CR16","unstructured":"Russell, N., ter Hofstede, A.H.M., Mulyar, N.: Workflow controlflow patterns: a revised view. In: BPM Center Report BPM-06-22, BPMcenter.org (2006)"},{"key":"149_CR17","doi-asserted-by":"crossref","unstructured":"Puhlmann, F., Weske, M.: Using the \u03c0-calculus for formalizing workflow patterns. In: Proceedings of BPM 2005. LNCS, vol. 3649, pp. 153\u2013168. Springer, Heidelberg (2005)","DOI":"10.1007\/11538394_11"},{"key":"149_CR18","doi-asserted-by":"crossref","unstructured":"Pomello, L., Rozenberg, G., Simone, C.: A survey of equivalence notions for net based systems. Advances in Petri Nets. LNCS, vol. 609, pp. 410\u2013472. Springer, Heidelberg (1992)","DOI":"10.1007\/3-540-55610-9_180"},{"key":"149_CR19","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"149_CR20","doi-asserted-by":"crossref","unstructured":"Billington, J., Christensen, S., van Hee, K., Kindler, E., Kummer, O., Petrucci, L., Post, R., Stehno, C., Weber, M.: The Petri Net markup language: concepts, technology, and tools. In: Proceedings of the ICATPN 2003. LNCS, vol. 2679, pp. 483\u2013505. Springer, Heidelberg (2003)","DOI":"10.1007\/3-540-44919-1_31"},{"key":"149_CR21","doi-asserted-by":"crossref","unstructured":"Karamanolis, C.T., Giannakopoulou, D., Magee, J., Wheater, S.M.: Model checking of workflow schemas. In: Proceedings of the 4th International Conference on Enterprise Distributed Object Computing, pp. 170\u2013181, IEEE Computer Society, USA (2000)","DOI":"10.1109\/EDOC.2000.882357"},{"issue":"2","key":"149_CR22","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0306-4379(00)00012-0","volume":"25","author":"W. Sadiq","year":"2000","unstructured":"Sadiq W., Orlowska M.E.: Analyzing process models using graph reduction techniques. Inf. Syst. 25(2), 117\u2013134 (2000)","journal-title":"Inf. Syst."},{"key":"149_CR23","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1088\/0967-1846\/3\/4\/002","volume":"3","author":"M. Kamathy","year":"1996","unstructured":"Kamathy M., Ramamrithamz K.: Correctness issues in workflow management. Distrib. Syst. Eng. 3, 213\u2013221 (1996)","journal-title":"Distrib. Syst. Eng."},{"key":"149_CR24","doi-asserted-by":"crossref","unstructured":"Ferrara, A.: Web services: a process algebra approach. In: Proceedings of the 2nd International Conference on Service Oriented Computing, pp. 242\u2013251. ACM Press, New York (2004)","DOI":"10.1145\/1035167.1035202"},{"issue":"7","key":"149_CR25","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1109\/TSE.2004.33","volume":"30","author":"R. Eshuis","year":"2004","unstructured":"Eshuis R., Wieringa R.: Tool support for verifying UML activity diagrams. IEEE Trans. Softw. Eng. 30(7), 437\u2013447 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"149_CR26","doi-asserted-by":"crossref","unstructured":"Fu, X., Bultan, T., Su, J.: Analysis of interacting BPEL web services. In: Proceedings of the 13th International Conference on World Wide Web, pp. 621\u2013630. ACM Press, New York (2004)","DOI":"10.1145\/988672.988756"},{"key":"149_CR27","doi-asserted-by":"crossref","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 W.M.P., Breutel S., Dumas M., ter Hofstede A.H.M.: Formal semantics and analysis of control flow in WS-BPEL. Sci. Comput. Program. 67, 162\u2013198 (2007)","journal-title":"Sci. Comput. Program."},{"key":"149_CR28","unstructured":"Fahland, D.: Translating UML2 Activity Diagrams to Petri Nets for Analyzing IBM WebSphere Business Modeler Process Models. Informatik-Berichte, 226. Humboldt-Universit\u00e4t zu Berlin (2008)"},{"issue":"3","key":"149_CR29","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1142\/S0218843004000973","volume":"13","author":"J. Dehnert","year":"2004","unstructured":"Dehnert J., van der Aalst W.M.P.: Bridging the gap between business models and workflow specifications. Int. J. Coop. Inf. Syst. 13(3), 289\u2013332 (2004)","journal-title":"Int. J. Coop. Inf. Syst."}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-010-0149-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-010-0149-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-010-0149-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T03:57:20Z","timestamp":1739851040000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-010-0149-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2,11]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,5]]}},"alternative-id":["149"],"URL":"https:\/\/doi.org\/10.1007\/s10270-010-0149-9","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2,11]]}}}