Verification of Business Process Quality Constraints Based on Visual Process Patterns
Verification of Business Process Quality Constraints Based on Visual Process Patterns
复制标题
基于可视化流程模式的业务流程质量约束验证
DOI：
10.1109/tase.2007.56
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Ragnhild Van Der Straeten
中科院分区：
文献类型：
--
作者：
A. Förster;G. Engels;Tim Schattkowsky;Ragnhild Van Der Straeten
业务流程通常必须考虑某些约束，如特定领域和质量要求。这些约束的自动化形式验证是可取的，但需要用户提供一个明确的正式规范。特别是，由于业务流程建模的符号通常是可视化的面向流的语言，因此与通常用于约束的正式规范的语言的符号差距，例如，时态逻辑是一个重要而又难以跨越的概念。因此，我们的方法依赖于UML活动作为一个单一的语言规范的业务流程和相应的约束。对于这种约束的表达，我们提供了一种基于专门活动的过程模式定义语言。在本文中，我们描述了如何模型检查可以用于对这些模式的业务流程的形式化验证。为此，我们提出了一个自动化的业务流程和相应的模式转换成一个过渡系统和时序逻辑，分别。
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.