Verification of Business Process Quality Constraints Based on Visual Process Patterns

Business processes usually have to consider certain constraints like domain specific and quality requirements. The automated formal verification of these constraints is desirable, 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 employed for the formal specification of constraints, e.g., temporal logic, is significant and hard to bridge. Thus, our approach relies on UML Activities as a single language for the specification of both business processes and the corresponding constraints. For the expression of such constraints, we have provided a process pattern definition language based on specialized Activities. In this paper, we describe how model checking can be employed for formal verification of business processes against such patterns. For this, we present an automated transformation of the business process and the corresponding patterns into a transition system and temporal logic, respectively.