Abstract
Security considerations, such as role-based access control (RBAC) mechanism and separation of duty (SoD) constraints, are important and integral to workflow systems. We propose the use of an equation-based method - The OTS/CafeOBJ method to specify workflow systems with such security considerations, and verify some desired safety and liveness properties of workflow systems. Specifically, a workflow system, together with its security considerations, is modeled as an OTS, a kind of transition system. Then the OTS is written in CafeOBJ, an algebraic specification language. We express safety and liveness properties in CafeOBJ and verify that the OTS satisfies these properties by writing proof scores in CafeOBJ. We use a case study - formal analysis of a workflow system that deals with travel expense reimbursement, to demonstrate our method of modeling, specifying and verifying.
| Original language | English |
|---|---|
| Title of host publication | 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005 |
| Pages | 531-536 |
| Number of pages | 6 |
| Publication status | Published - Dec 1 2005 |
| Event | 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005 - Taipei, Taiwan, Province of China Duration: Jul 14 2005 → Jul 16 2005 |
Publication series
| Name | 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005 |
|---|
Other
| Other | 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005 |
|---|---|
| Country | Taiwan, Province of China |
| City | Taipei |
| Period | 7/14/05 → 7/16/05 |
Fingerprint
All Science Journal Classification (ASJC) codes
- Software
Cite this
Formal analysis of workflow systems with security considerations. / Kong, Weiqiang; Ogata, Kazuhiro; Futatsugi, Kokichi.
17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005. 2005. p. 531-536 (17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Formal analysis of workflow systems with security considerations
AU - Kong, Weiqiang
AU - Ogata, Kazuhiro
AU - Futatsugi, Kokichi
PY - 2005/12/1
Y1 - 2005/12/1
N2 - Security considerations, such as role-based access control (RBAC) mechanism and separation of duty (SoD) constraints, are important and integral to workflow systems. We propose the use of an equation-based method - The OTS/CafeOBJ method to specify workflow systems with such security considerations, and verify some desired safety and liveness properties of workflow systems. Specifically, a workflow system, together with its security considerations, is modeled as an OTS, a kind of transition system. Then the OTS is written in CafeOBJ, an algebraic specification language. We express safety and liveness properties in CafeOBJ and verify that the OTS satisfies these properties by writing proof scores in CafeOBJ. We use a case study - formal analysis of a workflow system that deals with travel expense reimbursement, to demonstrate our method of modeling, specifying and verifying.
AB - Security considerations, such as role-based access control (RBAC) mechanism and separation of duty (SoD) constraints, are important and integral to workflow systems. We propose the use of an equation-based method - The OTS/CafeOBJ method to specify workflow systems with such security considerations, and verify some desired safety and liveness properties of workflow systems. Specifically, a workflow system, together with its security considerations, is modeled as an OTS, a kind of transition system. Then the OTS is written in CafeOBJ, an algebraic specification language. We express safety and liveness properties in CafeOBJ and verify that the OTS satisfies these properties by writing proof scores in CafeOBJ. We use a case study - formal analysis of a workflow system that deals with travel expense reimbursement, to demonstrate our method of modeling, specifying and verifying.
UR - http://www.scopus.com/inward/record.url?scp=67650082684&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=67650082684&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:67650082684
SN - 9781627486590
T3 - 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005
SP - 531
EP - 536
BT - 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005
ER -