Conflict detection and resolution for workflows constrained by resources and non-determined durations

The correctness of a workflow specification is critical for the automation of business processes. Therefore, errors in the specification should be detected and corrected at build-time. In this paper, we present a conflict verification and resolution approach for a kind of workflow constrained by resources and non-determined duration based on Petri net. In this kind of workflow, there are two timing functions for each activity to present the minimum and maximum duration of each activity, and the implementations of some activities require resources. Based on the Petri net model obtained, the earliest time to start each activity can be calculated and the key activities influencing the implementation of the workflow can be determined, with which the resource consistency between activities can be verified. Key-activity and waiting-short priority strategies are adopted to remove the resource conflicts between activities, which can ensure that most of the subsequent activities start as early as possible and that the whole workflow be finished in a shorter time. Through experiments, it is proved that the proposed removal strategy for resource conflicts is better than other strategies.     

需求信息管理的Petri网工作流模型

针对目前国内软件企业中需求信息管理存在的业务流程问题,提出合理的工作流建模方案。利用Petri网建模技术建立流程实例模型,再建立完整的工作流模型。按照Petri网的数学特性对结果模型进行的正确性分析和验证表明该模型具有良好的数学特性。基于Petri网的工作流建模方法能够为需求信息管理提供合理的解决方案。摘要:     

Classification and evaluation of timed running schemas for workflow based on process mining

The system running logs of a workflow contain much information about the behavior and logical structure between activities. In this paper, a mining approach is proposed to discover the structural and temporal model for a workflow from its timed running logs. The mining results are represented in the formalized form of Petri nets extended with two timing factors that allows validation or verification the actual behaviors, especially the temporal constraints between activities. According to the reachability graph of the extended Petri net model mined, all running schemas of a workflow can be generated, which defines the temporal constraints between running activities. By calculating the earliest and latest start time of each activity, the earliest starting and latest existing time of each state in the running schema can be determined. Based on the temporal relations between the timing factors of each running state, the running schemas can be classified into six classes. The effects of the six classes of running schemas on the implementation of the whole workflow are evaluated so as to obtain the best one that can ensure the workflow is finished in the shortest time. The standards for the ideal, reliable and favorable running schemas and their existence conditions are discussed, which can be used to evaluate the running logs and control the future running of a workflow.     

需求信息管理的Petri网工作流模型

针对目前国内软件企业中需求信息管理存在的业务流程问题．提出合理的工作流建模方案。利用Petri网建模技术建立流程实例模型,再建立完整的工作流模型。按照Petri网的数学特性对结果模型进行的正确性分析和验证表明该模型具有良好的数学特性。基于Petri网的工作流建模方法能够为需求信息管理提供合理的解决方案。     

Timing constraint workflow nets for workflow analysis

The analysis of the correctness and rationality of a workflow model plays an important role in the research of workflow techniques and successful implementation of workflow management. This paper points out the relevant problems in the verification and analysis of a workflow model. It discusses two important properties: schedulability and boundedness of a workflow model considering timing constraints. To specify the timing constraints, WorkFlow net is extended with time information, leading to timing constraint workflow net (TCWF-net). This paper presents a model mapping method to convert a directed network graph (DNG) based workflow model, which is built by a graphic process modeling language extended with time information, into a TCWF-net. It then discusses its schedulability verification and synthesis. An algorithm to decompose an acyclic and free-choice TCWF-net into a set of T-components is presented, followed by a boundedness verification method. The usefulness of the research results is illustrated by an example.     

Verifying workflow processes: a transformation-based approach

Workflow modeling is a challenging activity and designers are likely to introduce errors, especially in complex industrial processes. Effective process verification is essential at design time because the cost of fixing errors during runtime is substantially higher. However, most user-oriented workflow modeling languages lack formal semantics that hinders such verification. In this paper, we propose a generic approach based on the model transformation to verify workflow processes. The model transformation includes two steps: first, it formalizes the desirable semantics of each modeling element; secondly, it translates a workflow process with clear semantics to an equivalent Petri net. Thus, we can verify the original workflow process using existing Petri net theory and analysis tools. As a comprehensive case study, verifying workflow processes in an industrial modeling language (TiPLM) is presented. Experimental evaluations on verifying real-world business processes validate our approach.     

基于Petri网的建设工程项目实施阶段工作流建模与仿真

构建一个能够准确表达实施过程系统性、动态性和不确定性的工作流模型是实现建设工程项目实施阶段工作流管理与控制的有效途径。在对建设工程项目实施阶段工作流模型特点分析及工作流概念模型构建的基础上,基于分层赋时着色Petri网构建建设工程项目实施阶段工作流模型。通过运行该工作流模型,能够获得实施阶段的信息流、资源流、异常处理、持续时间等抽象内容,不仅为实现建设项目实施阶段的工作流管理与控制提供有力的方法支持,同时也是Petri网建模技术在建设工程领域中的应用拓广。借助CPN Tools仿真平台,以一般工业与民用建筑的实施阶段为例进行工作流模型的构建与仿真,验证了基于分层赋时着色Petri网构建建设工程项目实施阶段工作流模型的正确性和有效性。     

基于时间约束Petri网的工作流动态一致性检验

工作流系统中的时间管理是工作流建模和分析的重要组成部分。支持动态修改是人们在实际应用中对工作流系统提出的新要求。文中在基于时间约束的Petri网模型基础上,根据时间约束推理规则,提出一种动态修改时间约束时检验工作流一致性的方法,从而丰富了工作流的时间管理功能。     

基于时间约束Petri网的工作流可调度性分析

引入时间参数控制工作流高效执行是工作流技术研究的重要内容之一。在工作流的Petri网模型中引入时间参数,不仅可以对工作流中的活动进行时间约束,而且能建立相应的工作流时间约束Petri网模型。文中在分析该模型的时间约束和可调度性的基础上,提出了对工作流可调度性分析验证方法及其相应的算法,最后通过一个实例说明了分析验证的过程。     

基于Petri网的工作流过程建模

业务过程建模是整个工作流管理系统的基础,选择一种高效的建模技术对复杂多变的实际业务流程进行形式化表示对构建一个灵活的工作流管理系统起着至关重要的作用。本文利用了Petri网技术给业务过程建模,构造了一个灵活可分析的过程模型：首先介绍了相关的基于Petri网的工作流建模技术,接着描述了Petri网到工作流过程模型执行的映 射,然后给出了一个具体的基于Petri网建模方式的实例,最后利用随机Petri网和概率论的一些知识对该模型进行了时间性能分析。     

流程业务化定制中的工作流建模方法研究

针对流程业务化定制的需求,提出了一套面向业务人员的、直观易用的工作流建模方法.首先定义了一种基于有向图的工作流模型.在该模型的基础上,通过设置建模规则来规范业务人员的建模行为,使得无需模型验证就能够保证所建过程模型的正确性,从而回避了传统的有向图方法在模型分析方面的缺陷.最后将这套建模方法转化为Petri网的形式来描述,并利用Petri网的分析技术证明了该方法的可靠性.     

工作流模型的有向图表示及基于Petri网的验证方法

该文从工作流模型的基本结构出发，描述了模型结构的有向图表达方法与建模方式，提出了一种将有向图转化为Petri网的转换算法，说明Petri网与工作流网的关系，之后运用Petri网的分析技术来验证模型的正确性，为电子政务领域内工作流模型的正确性验证提供了一种解决方案。     

Verifying soundness of business processes: A decision process Petri nets approach

This paper presents a trajectory-tracking approach for verifying soundness of workflow/Petri nets represented by a decision-process Petri net. Well-formed business processes correspond to sound workflow nets. The advantage of this approach is its ability to represent the dynamic behavior of the business process. We show that the problem of finding an optimum trajectory for validation of well-formed business processes is solvable. To prove our statement we use the Lyapunov stability theory to tackle the soundness verification problem for decision-process Petri nets. As a result, applying Lyapunov theory, the well-formed verification (soundness) property is solved showing that the workflow net representation using decision process Petri nets is uniformly practically stable. It is important to note that in a complexity-theoretic sense checking the soundness property is computationally tractable, we calculate the computational complexity for solving the problem. We show the connection between workflow nets and partially ordered decision-process Petri net used for business process representation and analysis. Our computational experiment of supply chains demonstrate the viability of the modeling and solution approaches for solving computer science problems.     

工作流过程建模中的形式化验证技术

工作流过程建模是一个复杂且易错的过程．若过程定义在投入运行之后被发现有错,则修复错误的代价相当高,这个问题引起了研究界和工业界的高度重视．因此,在建模阶段进行有效的过程验证是十分必要的．综述了工作流过程验证技术的发展现状,包括强调验证的重要性,叙述了需要验证的问题和复杂度;介绍了对验证方法的要求;讨论了过程合理性验证和化简验证技术等;并通过对研究现状的分析和对比,提出了仍然没有解决的问题和将来的工作．     

时间约束工作流的可调度性分析

提出一种时间约束工作流的可调度性分析方法。针对时间约束Petri网（Timing Constraint Petri Nets,TCPN）为普通Petri网无法建模多参与资源的不足,给出了扩展的时间约束Petri网（w-TCPN）的定义;结合w-TCPN的拓扑结构,从模型和实例两个层次,给出了w-TCPN变迁可调度的判定定理;提出了时间约束的调整策略。w-TCPN的研究使得时间约束工作流的建模和可调度性分析更加合理。     

基于扩展Petri网的系统建模及形式化验证方法*

嵌入式实时系统对时间约束性、安全性和可靠性具有非常高的要求,但是传统的建模和形式化验证方法难以满足对系统的实时性和安全性的模拟和验证需求。通过对有色Petri网的时间属性进行扩展,提出了实时有色Petri网模型,能够对系统的时间属性进行模拟和评估;参考实时有色Petri网模型到时间自动机的语义转换规则对模型进行转换,可以利用时间计算树逻辑对系统的实时性、安全性和可靠性进行形式化验证。以列车通信网络控制器的双线冗余控制模块的建模和形式化验证为例,证明了该方法的有效性。     

基于反应型的Petri网工作流业务过程建模

传统的基于令牌机制的Petri网工作流模型虽然被广泛应用,但不能完整准确地反映工作流引擎运行时的实际情况。在充分考虑了系统运行时的实际场景之后,提出了一种基于反应型机制的Petri网工作流模型;然后分析了标准Petri网工作流模型到反应型Petri网工作流模型的转换方法和实现步骤,并给出了验证的思路。     

基于工作流的高校科研项目管理Petri网建模

科研项目管理是高校科研信息系统的核心部分之一,利用Petri网,对复杂的科研项目管理工作流程建模,解决高校信息化中较为复杂的科研项目管理工作流问题。以高校科研项目申请流程为例,给出了相关定义,分析和解决建模中遇到的几个问题。     

基于Petri 网的工业设计过程管理工作流建模研究

工业设计过程建模是产品设计过程管理研究的关键环节,直接影响着项目开发周 期和整体效益,但目前工业设计行业没有针对设计过程管理有效的建模技术及其系统。为实现 对工业设计企业设计过程动态性、结构性和有序性管理,在产品设计过程管理中引入面向过程 的组织管理与流程优化的工作流技术及Petri 网建模方法;然后根据对设计过程管理流程的研 究,构建了设计过程管理工作流程图;进而结合工作流技术、Petri 网过程建模方法和工业设计 过程管理流程提出工业设计过程管理的4 个阶段工作流建模方法：本体分析、元素提取、元素 概括、元素带入;最后,以工业设计过程管理建模领域为例构建了基于Petri 网的工业设计过程 管理工作流模型,在此基础上实现了工业设计过程管理原型系统。     

基于HTCPN的工程项目群工作流建模与仿真

在工程项目群实施阶段框架模型构建的基础上, 基于分层赋时着色Petri网定义了工程项目群实施阶段工作流模型。借助CPN Tools仿真平台, 以某工程项目群实施阶段为例进行了实例建模与仿真, 验证了基于分层赋时着色Petri网构建工程项目群实施阶段工作流模型的有效性。该工作流模型能够全面、准确地描述项目群复杂系统的实施全过程, 为实现项目群管理中的进度风险分析和流程优化提供技术与方法的支持。