Formal analysis of workflow systems with security considerations

Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi

    Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
    Title of host publication17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005
    Pages531-536
    Number of pages6
    Publication statusPublished - Dec 1 2005
    Event17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005 - Taipei, Taiwan, Province of China
    Duration: Jul 14 2005Jul 16 2005

    Publication series

    Name17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005

    Other

    Other17th International Conference on Software Engineering and Knowledge Engineering, SEKE 2005
    CountryTaiwan, Province of China
    CityTaipei
    Period7/14/057/16/05

    All Science Journal Classification (ASJC) codes

    • Software

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

    Cite this