{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T21:55:05Z","timestamp":1761947705396},"reference-count":13,"publisher":"World Scientific Pub Co Pte Lt","issue":"07","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2010,11]]},"abstract":"<jats:p> Business Process Modeling Notation (BPMN) plays a significant role in the specification of business processes. To ascertain the validity of BPMN models, a disciplined approach to analyze their behavior is of particular interest to the field of business process management. This paper advocates a semantics-preserving method for transforming BPMN models into New Symbolic Model Verifier (NuSMV) language as a means to verify the models. A subset of BPMN is specified rigorously in the form of a mathematical model. With this foundation in place, the translation for the subset of BPMN notational elements is then driven by a set of formally defined rules. The practicality of our approach is exemplified using an on-line flight reservation service. <\/jats:p>","DOI":"10.1142\/s0218194010005079","type":"journal-article","created":{"date-parts":[[2011,3,22]],"date-time":"2011-03-22T10:48:13Z","timestamp":1300790893000},"page":"987-1023","source":"Crossref","is-referenced-by-count":13,"title":["FORMAL ANALYSIS OF BPMN MODELS: A NuSMV-BASED APPROACH"],"prefix":"10.1142","volume":"20","author":[{"given":"VITUS S. W.","family":"LAM","sequence":"first","affiliation":[{"name":"Computer Centre, The University of Hong Kong, Pokfulam Road, Hong Kong"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2012,4,30]]},"reference":[{"key":"rf1","volume-title":"Essential Business Process Modeling","author":"Havey M.","year":"2005"},{"key":"rf4","volume-title":"Business Process Execution Language for Web Services","author":"Juric M. B.","year":"2006"},{"key":"rf5","first-page":"43","volume":"14","author":"Lam V. S. W.","journal-title":"Nordic Journal of Computing"},{"key":"rf7","doi-asserted-by":"publisher","DOI":"10.1080\/00207540701199677"},{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2008.02.006"},{"key":"rf15","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985"},{"key":"rf17","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.06.029"},{"key":"rf18","volume-title":"Science of Computer Programming","author":"Wong P. Y. H.","year":"2009"},{"key":"rf19","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999"},{"key":"rf22","doi-asserted-by":"publisher","DOI":"10.1007\/s11761-009-0048-5"},{"key":"rf23","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"rf24","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275"},{"key":"rf26","volume-title":"Discrete Mathematics","author":"Johnsonbaugh R.","year":"1986"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194010005079","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T15:58:42Z","timestamp":1565107122000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194010005079"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11]]},"references-count":13,"journal-issue":{"issue":"07","published-online":{"date-parts":[[2012,4,30]]},"published-print":{"date-parts":[[2010,11]]}},"alternative-id":["10.1142\/S0218194010005079"],"URL":"https:\/\/doi.org\/10.1142\/s0218194010005079","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,11]]}}}