{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T09:45:12Z","timestamp":1781343912299,"version":"3.54.1"},"reference-count":34,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"funder":[{"DOI":"10.13039\/501100002873","name":"Chulalongkorn University","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002873","id-type":"DOI","asserted-by":"publisher"}]},{"name":"90th Anniversary of Chulalongkorn University Fund"},{"name":"Overseas Research Experience Scholarship for Graduate Student"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2019]]},"DOI":"10.1109\/access.2019.2892958","type":"journal-article","created":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T19:45:37Z","timestamp":1547495137000},"page":"16795-16815","source":"Crossref","is-referenced-by-count":28,"title":["Hierarchical Verification for the BPMN Design Model Using State Space Analysis"],"prefix":"10.1109","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8441-8962","authenticated-orcid":false,"given":"C.","family":"Dechsupa","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"W.","family":"Vatanawood","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A.","family":"Thongtak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99840-4_5"},{"key":"ref32","year":"2018","journal-title":"The BPMN Modeler"},{"key":"ref31","article-title":"The minimal coverability graph for Petri nets","author":"finkel","year":"1993","journal-title":"Advances in Petri Nets"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/UCC.2014.34"},{"key":"ref34","first-page":"219","article-title":"A holistic approach for soundness verification of decision-aware process models (extended version)","author":"de leoni","year":"2018","journal-title":"Proc ER"},{"key":"ref10","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1002\/9781119991472"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-4223-X"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.4249\/scholarpedia.6477"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_31"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.12.036"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1080\/00207540701199677"},{"key":"ref17","first-page":"1","article-title":"Formal semantics of BPMN process models using CPN","volume":"5","author":"ibrahim","year":"2017","journal-title":"IREIT"},{"key":"ref18","first-page":"1","article-title":"BPMN Formalisation using coloured Petri nets","author":"ramadan","year":"2011","journal-title":"Proc 2nd GSTF Annu Int Conf Softw Eng Appl"},{"key":"ref19","article-title":"Formal semantics and analysis of BPMN process models using Petri nets","author":"dijkman","year":"2007"},{"key":"ref28","year":"2015","journal-title":"UPPAAL"},{"key":"ref4","volume":"37","author":"jensen","year":"2008","journal-title":"Coloured Petri Nets Basic Concepts Analysis Methods and Practical Use"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2015.2413401"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","article-title":"Coloured Petri nets and CPN tools for modelling and validation of concurrent systems","volume":"9","author":"jensen","year":"2007","journal-title":"Int J Softw Tools Technol Transf"},{"key":"ref6","first-page":"398","article-title":"Formal verification of web service orchestration using colored Petri net","volume":"1","author":"dechsupa","year":"2016","journal-title":"Proc Int Eng Comput Scientists MultiConf"},{"key":"ref29","year":"2013","journal-title":"VerChor Framework"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2018.2853669"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46397-1_27"},{"key":"ref7","article-title":"Analyzing control-flow and data-flow in workflow processes in a unified way","volume":"831","author":"tr?ka","year":"2008"},{"key":"ref2","first-page":"1","author":"clarke","year":"2012","journal-title":"Progress on the State Explosion Problem in Model Checking"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ICSEC.2014.6978226"},{"key":"ref1","year":"2015","journal-title":"Unified Modeling Language (OMG UML) Version 2 5"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2016.12.044"},{"key":"ref22","author":"boucheneb","year":"2018","journal-title":"Model Checking of Time Petri Nets"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.20532\/cit.2016.1002774"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-642-12186-9_2","article-title":"Diagnosing and repairing data anomalies in process models","volume":"43","author":"awad","year":"2010","journal-title":"Lecture Notes in Business Information Processing"},{"key":"ref23","first-page":"1","article-title":"Detecting data-flow errors in BPMN 2.0","volume":"1","author":"von stackelberg","year":"2014","journal-title":"Open Inf Syst"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/AICCSA.2015.7507176"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1080\/17517575.2013.879211"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/8600701\/08611325.pdf?arnumber=8611325","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,27]],"date-time":"2022-01-27T07:43:29Z","timestamp":1643269409000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8611325\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"references-count":34,"URL":"https:\/\/doi.org\/10.1109\/access.2019.2892958","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]}}}