Verification of Business Process Quality Constraints Based on Visual Process Patterns

Alexander Foerster, Gregor Engels, Tim Schattkowsky, Ragnhild Van Der Straeten

    Onderzoeksoutput: Conference paper

    67 Citaten (Scopus)


    Business processes usually have to consider certain con-
    straints like domain specific and quality requirements. The
    automated formal verification of these constraints is de-
    sirable, but requires the user to provide an unambiguous
    formal specification. In particular since the notations for
    business process modeling are usually visual flow-oriented
    languages, the notational gap to the languages usually em-
    ployed for the formal specification of constraints, e.g., tem-
    poral logic, is significant and hard to bridge. Thus, our ap-
    proach relies on UML Activities as a single language for
    the specification of both business processes and the cor-
    responding constraints. For the expression of such con-
    straints, we have provided a process pattern definition lan-
    guage based on specialized Activities. In this paper, we de-
    scribe how model checking can be employed for formal ver-
    ification of business processes against such patterns. For
    this, we present an automated transformation of the busi-
    ness process and the corresponding patterns into a transi-
    tion system and temporal logic, respectively.
    Originele taal-2English
    TitelFirst Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007
    UitgeverijIEEE Computer Society Press
    StatusPublished - 2007
    EvenementUnknown - Stockholm, Sweden
    Duur: 21 sep 200925 sep 2009




    Duik in de onderzoeksthema's van 'Verification of Business Process Quality Constraints Based on Visual Process Patterns'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit