{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,25]],"date-time":"2022-04-25T02:04:39Z","timestamp":1650852279184},"reference-count":7,"publisher":"World Scientific Pub Co Pte Lt","issue":"01","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2007,2]]},"abstract":"<jats:p> Security considerations, such as role-based access control (RBAC) mechanism and separation of duty (SoD) constraints, are important and integral to workflow systems. Since the definition of workflows with these security considerations is a complicated and error-prone process, rigorous verification techniques are desirable for uncovering logical errors and assuring correctness. We propose the use of an equation-based method \u2014 the OTS\/CafeOBJ method to model, specify and verify workflows with such security considerations. Specifically, a workflow with the security considerations, is modeled as an OTS, a kind of transition system; the OTS is then specified in CafeOBJ, an algebraic specification language. We verify that the OTS has desired safety and liveness properties by using the CafeOBJ system as an interactive theorem prover. A case study on a sample workflow that deals with travel expense reimbursement is used to demonstrate our method. <\/jats:p>","DOI":"10.1142\/s0218194007003124","type":"journal-article","created":{"date-parts":[[2007,3,26]],"date-time":"2007-03-26T10:12:09Z","timestamp":1174903929000},"page":"3-32","source":"Crossref","is-referenced-by-count":5,"title":["SPECIFICATION AND VERIFICATION OF WORKFLOWS WITH RBAC MECHANISM AND SoD CONSTRAINTS"],"prefix":"10.1142","volume":"17","author":[{"given":"WEIQIANG","family":"KONG","sequence":"first","affiliation":[{"name":"Graduate School of Information Science, Japan Advanced Institute of Science and Technology, 1-1, Asahidai, Nomi, Ishikawa 923-1292, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"KAZUHIRO","family":"OGATA","sequence":"additional","affiliation":[{"name":"Graduate School of Information Science, Japan Advanced Institute of Science and Technology, 1-1, Asahidai, Nomi, Ishikawa 923-1292, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"KOKICHI","family":"FUTATSUGI","sequence":"additional","affiliation":[{"name":"Graduate School of Information Science, Japan Advanced Institute of Science and Technology, 1-1, Asahidai, Nomi, Ishikawa 923-1292, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf3","doi-asserted-by":"publisher","DOI":"10.1145\/300830.300837"},{"key":"rf5","series-title":"Texts and Monographs in Computer Science","volume-title":"A Logical Approach to Discrete Math","author":"David G.","year":"1993"},{"key":"rf6","doi-asserted-by":"publisher","DOI":"10.1142\/3831"},{"key":"rf7","volume-title":"Workflow Handbook 1997","author":"Lawrence P.","year":"1997"},{"key":"rf10","volume-title":"Parallel Program Design: A Foundation","author":"Mani Chandy J. M. K.","year":"1988"},{"key":"rf23","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022883727209"},{"key":"rf24","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/44.4.246"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194007003124","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T01:47:36Z","timestamp":1565142456000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194007003124"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2]]},"references-count":7,"journal-issue":{"issue":"01","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2007,2]]}},"alternative-id":["10.1142\/S0218194007003124"],"URL":"https:\/\/doi.org\/10.1142\/s0218194007003124","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2]]}}}