Formal analysis of workflow systems with security considerations

Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi

研究成果: 著書/レポートタイプへの貢献会議での発言

1 引用 (Scopus)

抜粋

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.

元の言語英語
ホスト出版物のタイトル17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005
ページ531-536
ページ数6
出版物ステータス出版済み - 12 1 2005
イベント17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005 - Taipei, 台湾省、中華民国
継続期間: 7 14 20057 16 2005

出版物シリーズ

名前17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005

その他

その他17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005
台湾省、中華民国
Taipei
期間7/14/057/16/05

    フィンガープリント

All Science Journal Classification (ASJC) codes

  • Software

これを引用

Kong, W., Ogata, K., & Futatsugi, K. (2005). Formal analysis of workflow systems with security considerations. : 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).