Formal analysis of workflow systems with security considerations

Weiqiang Kong; Kazuhiro Ogata; Kokichi Futatsugi

Formal analysis of workflow systems with security considerations

Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi

Research and Development Center for Smart Mobility

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

1 Citation (Scopus)

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

All Science Journal Classification (ASJC) codes

Software

Access to Document

Fingerprint Dive into the research topics of 'Formal analysis of workflow systems with security considerations'. Together they form a unique fingerprint.

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

Kong, W, Ogata, K & Futatsugi, K 2005, Formal analysis of workflow systems with security considerations. in 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005. 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005, pp. 531-536, 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005, Taipei, Taiwan, Province of China, 7/14/05.

@inproceedings{1933e510045f44be8e745e752784aaea,

title = "Formal analysis of workflow systems with security considerations",

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.",

author = "Weiqiang Kong and Kazuhiro Ogata and Kokichi Futatsugi",

year = "2005",

month = dec,

day = "1",

language = "English",

isbn = "9781627486590",

series = "17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005",

pages = "531--536",

booktitle = "17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005",

note = "17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005 ; Conference date: 14-07-2005 Through 16-07-2005",

}

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

T2 - 17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005

Y2 - 14 July 2005 through 16 July 2005

ER -