Soundness-preserving reduction rules for reset workflow nets

The application of reduction rules to any Petri net may assist in its analysis as its reduced version may be significantly smaller while still retaining the original net’s essential properties. Reset nets extend Petri nets with the concept of a reset arc, allowing one to remove all tokens from a certain place. Such nets have a natural application in business process modelling where possible cancellation of activities need to be modelled explicitly and in workflow management where such process models with cancellation behaviours should be enacted correctly. As cancelling the entire workflow or even cancelling certain activities in a workflow has serious implications during execution (for instance, a workflow can deadlock because of cancellation), such workflows should be thoroughly tested before deployment. However, verification of large workflows with cancellation behaviour is time consuming and can become intractable due to the state space explosion problem. One way of speeding up verification of workflows based on reset nets is to apply reduction rules. Even though reduction rules exist for Petri nets and some of its subclasses and extensions, there are no documented reduction rules for reset nets. This paper systematically presents such reduction rules. Because we want to apply the results to the workflow domain, this paper focusses on reset workflow nets (RWF-nets), i.e. a subclass tailored to the modelling of workflows. The approach has been implemented in the context of the workflow system YAWL.     

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.     

精炼工作流网的行为保持性质

本文定义了工作流网的精炼操作，研究了精炼工作流网的行为保持性质。结果表明精炼工作流网满足行为保持性质，即精炼工作流网的行为与原网和子网行为保持一致。在精炼工作流网行为保持性质的基础上，给出了基于原网语言和子网语言的精炼工作流网的语言刻画。本文结果有助于复杂工作流的设计、建模和验证。     

Verification problems in conceptual workflow specifications

Most of today's business requirements can only be accomplished through integration of various autonomous systems which were initially designed to serve the needs of particular applications. In the literature workflows are proposed to design these kinds of applications. The key tool for designing such applications is a powerful conceptual specification language. Such a language should be capable of capturing interactions and cooperation between component tasks of workflows among others. These include sequential execution, iteration, choice, parallelism and synchronisation. The central focus of this paper is the verification of such process control aspects in conceptual workflow specifications. As is generally agreed upon, that the later in the software development process an error is detected, the more it will cost to correct it; it is thus of vital importance to detect errors as early as possible in the systems-development process. In this paper some typical verification problems in workflow specifications are identified and their complexity is addressed. It will be proven that some fundamental problems are not tractable and we will show what restriction is needed to allow termination problems to be recognized in polynomial time.     

YAWL: yet another workflow language

Based on a rigorous analysis of existing workflow management systems and workflow languages, a new workflow language is proposed: yet another workflow language (YAWL). To identify the differences between the various languages, we have collected a fairly complete set of workflow patterns. Based on these patterns we have evaluated several workflow products and detected considerable differences in their ability to capture control flows for non-trivial workflow processes. Languages based on Petri nets perform better when it comes to state-based workflow patterns. However, some patterns (e.g. involving multiple instances, complex synchronisations or non-local withdrawals) are not easy to map onto (high-level) Petri nets. This inspired us to develop a new language by taking Petri nets as a starting point and adding mechanisms to allow for a more direct and intuitive support of the workflow patterns identified. This paper motivates the need for such a language, specifies the semantics of the language, and shows that soundness can be verified in a compositional way. Although YAWL is intended as a complete workflow language, the focus of this paper is limited to the control-flow perspective.     

Specification of behavioral anti-patterns for the verification of block-structured Collaborative Business Processes

Context: The verification of the control flow of a Collaborative Business Process (CBP) is important when developing cross-organizational systems, since the control flow defines the behavior of the cross-organizational collaboration. Behavioral anti-patterns have been proposed to improve the performance of formal verification methods. However, a systematic approach for the discovery and specification of behavioral anti-patterns of CBPs has not been proposed so far.Objective: The aim of this work is an approach to systematically discover and specify the behavioral anti-patterns of block-structured CBP models.Method: The approach proposes using the metamodel of a CBP language to discover all possible combinations of constructs leading to a problem in the behavior of block-structured CBPs. Each combination is called minimal CBP. The set of all minimal CBPs with behavioral problems defines the unsoundness profile of a CBP language, from which is possible specifying the behavioral anti-patterns of such language.Results: The approach for specification of behavioral anti-patterns was applied to the UP-ColBPIP language. Twelve behavioral anti-patterns were defined, including support to complex control flow such as advanced synchronization, cancellation and exception management, and multiple instances. Anti-patterns were evaluated on a repository of block-structured CBP models and compared with a formal verification method. Results show that the verification based on anti-patterns is as accurate as the formal method, but it clearly improves the performance of the latter.Conclusion: By using the proposed approach, it is possible to systematically specify behavioral anti-patterns for block-structured CBP languages. During the discovery of anti-patterns different formalisms can be used. With this approach, the specification of anti-patterns provides the exact combination of elements that can cause a problem, making error correction and result interpretation easier. Although the proposed approach was defined for the context of CBPs, it could be applied to the context of intra-organizational processes.     

Workflow Patterns

Differences in features supported by the various contemporary commercial workflow management systems point to different insights of suitability and different levels of expressive power. The challenge, which we undertake in this paper, is to systematically address workflow requirements, from basic to complex. Many of the more complex requirements identified, recur quite frequently in the analysis phases of workflow projects, however their implementation is uncertain in current products. Requirements for workflow languages are indicated through workflow patterns. In this context, patterns address business requirements in an imperative workflow style expression, but are removed from specific workflow languages. The paper describes a number of workflow patterns addressing what we believe identify comprehensive workflow functionality. These patterns provide the basis for an in-depth comparison of a number of commercially availablework flow management systems. As such, this paper can be seen as the academic response to evaluations made by prestigious consulting companies. Typically, these evaluations hardly consider the workflow modeling language and routing capabilities, and focus more on the purely technical and commercial aspects.     

Applying Propositional Logic to Workflow Verification

The increasing complexity of business processes in the era of e-business has heightened the need for workflow verification tools. However, workflow verification remains an open and challenging research area. As an indication, most of commercial workflow management systems do not yet provide workflow designers with formal workflow verification tools. We propose a logic-based verification method that is based on a well-known formalism, i.e., propositional logic. Our logic-based workflow verification approach has distinct advantages such as its rigorous yet simplistic logical formalism and its ability to handle generic activity-based process models. In this paper, we present the theoretical framework for applying propositional logic to workflow verification and demonstrate that logic-based workflow verification is capable of detecting process anomalies in workflow models.     

On verification of nested workflows with extra constraints: From theory to practice

Workflows are used to formally describe processes of various types such as business and manufacturing processes. One of the critical tasks of workflow management is automated discovery of possible flaws in the workflow – workflow verification. In this paper, we formalize the problem of workflow verification as the problem of verifying that there exists a feasible process for each task in the workflow. This problem is tractable for nested workflows that are the workflows with a hierarchical structure similar to hierarchical task networks in planning. However, we show that if extra synchronization, precedence, or causal constraints are added to the nested structure, the workflow verification problem becomes NP-complete. We present a workflow verification algorithm for nested workflows with extra constraints that is based on constraint satisfaction techniques and exploits an incremental temporal reasoning algorithm. We then experimentally demonstrate efficiency of the proposed techniques on randomly generated workflows with various structures and sizes. The paper is concluded by notes on exploiting the presented techniques in the application FlowOpt for modeling, optimizing, visualizing, and analyzing production workflows.     

纯SV语言搭建验证平台

面对日益复杂的芯片系统设计和IP的高度集成方式,验证的重要性日益增加。传统的验证主要依赖于直接测试,虽然直接测试平台也可以采用有限的随机方式,但是通常是通过产生随机数的方式来实现的,而不是在每个数据单元简单地写入预先设定的值。直接测试方法适合于小设计,但一个典型SoC设计需要上千个测试用例,耗时太长。因此提升验证产量的唯一方法是减少产生测试所消耗时间。基于SystemVerilog具有丰富语言能力、能描述复杂验证环境、产生带约束的随机激励、面向对象编程、功能覆盖率统计等诸多优点,因此可以采用SystemVerilog语言功能构建一个验证平台。搭建验证环境时,可以应用带约束随机激励产生方法以及覆盖率驱动来提高验证效率,缩短验证周期,平台在queastasim上进行了仿真验证,并取得了比较好的结果。     

On design,verification, and dynamic modification of the problem-based scientific workflow model

A science process is a process to solve complex scientific problems which usually have no mature solving methods. Science processes if modeled in workflow forms, i.e. scientific workflows, can be managed more effectively and performed more automatically. However, most current workflow models seldom take account of specific characteristics of science processes and are not very suitable for modeling scientific workflows. Therefore, a new workflow model named problem-based scientific workflow model (PBSWM) is proposed in this paper to accommodate those specific characteristics. Corresponding soundness verification and dynamic modification are discussed accordingly based on the new modelling method. This paper makes three main contributions: (1) three new constructs are proposed for special logic semantics in science processes; (2) verification is deployed with the consideration from both data-specific perspective and control-specific perspective; and (3) a set of rules are provided to automatically infer passive modifications caused by other modifications.     

Petri net based Grid workflow verification and optimization

Graphical workflow modeling tools, such as UML and DAG, can facilitate users to express workflow process logic, but lack of abilities to carry out simulation and correctness checking. In this paper, based on Petri net, we propose a service composition oriented Grid workflow model and its related six elementary workflow patterns: sequence, condition, iteration, concurrency, synchronization, and triggering. In addition, we present our Grid workflow analysis approaches on three aspects: workflow reachability verification, workflow deadlock verification, and workflow optimization. The experimental results show that our workflow verification and optimization mechanisms are feasible and efficient.     

Modeling and Analysis for Workflow Constrained by Resources and Nondetermined Time: An Approach Based on Petri Nets

Time and resource management and verification are two important aspects of workflow management systems. In this paper, we present a modeling and analysis approach for a kind of workflow constrained by resources and nondetermined time based on Petri nets. Different from previous modeling approaches, there are two kinds of places in our model to represent the activities and resources of a workflow, respectively. For each activity place, its input and output transitions represent the start and termination of the activity, respectively, and there are two timing functions in it to define the minimum and maximum duration times of the corresponding activity. Using the constructed Petri net model, the earliest and latest times to start each activity can be calculated. With the reachability graph of the Petri net model, the timing factors influencing the implementation of the workflow can be calculated and verified. In this paper, the sufficient conditions for the existence of the best implementation case of a workflow are proved, and the method for obtaining such an implementation case is presented. The obtained results will benefit the evaluation and verification of the implementation of a workflow constrained by resources and nondetermined time.     

A practical method to analyze workflow logic models

The analysis of workflow is crucial to the correctness of workflow applications. This paper introduces a simple and practical method for analyzing workflow logic models. Firstly, some definitions of the models and some properties, such as throughness, no‐redundant‐transition and boundedness, are presented. Then, we propose an approach based on synchronized reachability graphs (SRGs) to verify these properties. The SRG uses the characteristics of synchronizers in workflow logic models and mitigates the state explosion by constructing synchronized occurrence sequences rather than interleaving occurrence sequences. This paper also proposes some refined and feasible reduction rules which can preserve vital properties of workflow logic models. Using these two techniques, the SRG‐based verification method can achieve higher efficiency. Furthermore, this research also develops a verification tool based on the method, presents the analysis results of some practical cases and compares our method with others. Copyright © 2007 John Wiley & Sons, Ltd.     

扩展的高层次行为描述内部模型

随着片上系统(SOC)技术的发展,越来越多的功能模块被集成到单一芯片中。适合硬件描述的HDL语言很难满足实现复杂算法功能的要求,C++等高级语言可以高效地描述算法功能,但是在综合和验证时遇到很大困难。文章介绍了一种允许使用C和VHDL独立描述原始模块,通过创建统一内部模型IIR的办法实现对功能元件和算法模块的混合处理。IIR内部模型以XML文件格式作为外部存储,能够方便地被划分、综合、验证等处理程序使用,避免了重复的原始描述文件分析,提高了研发效率。     

Ontology-based requirement verification for complex systems

Verification is a necessary part of Model-based systems engineering (MBSE) which is becoming a mainstream methodology for the design of complex systems. Verification in the early design stage has aroused widespread attention for its efficiency and cost-saving. Although there are numbers of researches on verification, some deficiencies still exist, such as the integration of design and verification needs to improve, the design problems are hard to trace and the behavior verification in the early design stage is often omitted. In this study, a novel ontology-based requirement verification method for complex systems is proposed to solve the above-mentioned problems. First, a requirement formalization method is proposed to avoid the ambiguousness of natural language, to make requirements easier to verify, and to make design problems easier to trace. Second, some transformation rules are defined to realize the automatic design ontology and rule generation. Based on these two steps, automated verification can be done through reasoning with ontology models and rules. This verification method is fully integrated with design tools and no additional expertise is needed for designers. To validate its feasibility and advantages, an example of a smart traffic light system is provided.     

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.     

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网的工作流模型分析

工作流管理的最终目的是实现适当的人在适当的时间执行适当的活动.企业要获得竞争力,需要在工作流模型中考虑与业务过程相关的时间约束.一个考虑时间因素的工作流模型,需要在投入运行前进行时间规范与验证,以保证工作流执行的时间协调.通过为工作流网元素扩展时间属性,得到集成业务过程时间约束的工作流模型??时间约束工作流网(TCWF-nets).基于对业务活动的可调度性分析,提出了时序一致性验证方法,确保工作流执行中活动之间时间交互的安全性.在所附加的时间约束下,该可调度分析方法不仅能够检测某一给定工作流调度的时间可行性,还能对特定的实例给出一个最优调度,使工作流执行延迟最小.研究结果表明,该方法支持业务过程的时间建模与分析,对于丰富现有工作流系统的时间管理功能以及增强现存工作流软件对动态业务环境的适应性具有重要意义.