TY - JOUR
T1 - Specification and verification of workflows with RBAC mechanism and SoD constraints
AU - Kong, Weiqiang
AU - Ogata, Kazuhiro
AU - Futatsugi, Kokichi
N1 - Funding Information:
This research is conducted as a program for the “21st Century COE Program” in Special Coordination Funds for promoting Science and Technology by Ministry of Education, Culture, Sports, Science and Technology. We would like to thank Mark G. Elwell for his help in proofreading the paper.
PY - 2007/2
Y1 - 2007/2
N2 - 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 - the OTS/Cafe OBJ 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.
AB - 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 - the OTS/Cafe OBJ 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.
UR - http://www.scopus.com/inward/record.url?scp=33947671905&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33947671905&partnerID=8YFLogxK
U2 - 10.1142/S0218194007003124
DO - 10.1142/S0218194007003124
M3 - Article
AN - SCOPUS:33947671905
SN - 0218-1940
VL - 17
SP - 3
EP - 32
JO - International Journal of Software Engineering and Knowledge Engineering
JF - International Journal of Software Engineering and Knowledge Engineering
IS - 1
ER -