Consistency degree calculation is established on the basis of known correspondence, but in real life, the correspondence is generally unknown, so how to calculate consistency of two models under unknown correspondence...Consistency degree calculation is established on the basis of known correspondence, but in real life, the correspondence is generally unknown, so how to calculate consistency of two models under unknown correspondence has become a problem. For this condition, we should analyze unknown correspondence due to the influence of different correspondences.In this paper we obtain the relations of transitions based on event relations using branching processes, and build a behavioral matrix of relations. Based on the permutation of behavioral matrix, we express different correspondences, and define a new formula to compute the maximal consistency degree of two workflow nets. Additionally, this paper utilizes an example to show these definitions, computation as well as the advantages.展开更多
The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic （CTL） allows us to verify the soundness with symbolic model checkers. Therefore t...The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic （CTL） allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic ＊ （CTL ＊ ） can be used to character the relaxed soundness of the workflow.展开更多
In a cloud-native era,the Kubernetes-based workflow engine enables workflow containerized execution through the inherent abilities of Kubernetes.However,when encountering continuous workflow requests and unexpected re...In a cloud-native era,the Kubernetes-based workflow engine enables workflow containerized execution through the inherent abilities of Kubernetes.However,when encountering continuous workflow requests and unexpected resource request spikes,the engine is limited to the current workflow load information for resource allocation,which lacks the agility and predictability of resource allocation,resulting in over and underprovisioning resources.This mechanism seriously hinders workflow execution efficiency and leads to high resource waste.To overcome these drawbacks,we propose an adaptive resource allocation scheme named adaptive resource allocation scheme(ARAS)for the Kubernetes-based workflow engines.Considering potential future workflow task requests within the current task pod’s lifecycle,the ARAS uses a resource scaling strategy to allocate resources in response to high-concurrency workflow scenarios.The ARAS offers resource discovery,resource evaluation,and allocation functionalities and serves as a key component for our tailored workflow engine(KubeAdaptor).By integrating the ARAS into KubeAdaptor for workflow containerized execution,we demonstrate the practical abilities of KubeAdaptor and the advantages of our ARAS.Compared with the baseline algorithm,experimental evaluation under three distinct workflow arrival patterns shows that ARAS gains time-saving of 9.8% to 40.92% in the average total duration of all workflows,time-saving of 26.4% to 79.86% in the average duration of individual workflow,and an increase of 1% to 16% in centrol processing unit(CPU)and memory resource usage rate.展开更多
In this paper, we propose astochastic Petri net model P-timed Workflow (WPTSPN) to specify, verify, and analyze a business process (BP) of a Flexible Manufacturing System (FMS). After formalizing the semantics of our ...In this paper, we propose astochastic Petri net model P-timed Workflow (WPTSPN) to specify, verify, and analyze a business process (BP) of a Flexible Manufacturing System (FMS). After formalizing the semantics of our model, we illustrate how to verifysome of its properties (reachability, safety, boundedness, liveness, correctness, alive tokens, and security) in the P-Timed context. Next, we validate the relevance of the proposed model with MATLAB simulation through a specific FMS case study. Finally, we use a generalized truncated density function to predict the duration of a token’s sojourn (residence) in a timed place with respect to the sequence states of the global FMS workflow.展开更多
Access control is an important protection mechanism for information systems. This paper shows how to make access control in workflow system. We give a workflow access control model (WACM) based on several current acce...Access control is an important protection mechanism for information systems. This paper shows how to make access control in workflow system. We give a workflow access control model (WACM) based on several current access control models. The model supports roles assignment and dynamic authorization. The paper defines the workflow using Petri net. It firstly gives the definition and description of the workflow, and then analyzes the architecture of the workflow access control model (WACM). Finally, an example of an e-commerce workflow access control model is discussed in detail.展开更多
Workflow management is concerned with automated support for business processes.Workflow management systems are driven by process models specifying the tasks that need to be executed,the order in which they can be exec...Workflow management is concerned with automated support for business processes.Workflow management systems are driven by process models specifying the tasks that need to be executed,the order in which they can be executed,which resources are authorised to perform which tasks,and data that is required for,and produced by,these tasks.As workflow instances may run over a sustained period of time,it is important that workflow specifications be checked before they are deployed.Workflow verification is usually concerned with control-flow dependencies only;however,transition conditions based on data may further restrict possible choices between tasks.In this paper we extend workflow nets where transitions have concrete conditions associated with them,called WTC-nets.We then demonstrate that we can determine which execution paths of a WTC-net that are possible according to the control-flow dependencies,are actually possible when considering the conditions based on data.Thus,we are able to more accurately determine at design time whether a workflow net with transition conditions is sound.展开更多
The correctness of workflow models is one of the major challenges in context of workflow analysis. The aim of this paper is to provide an improved Petri net-based reduction approach for verifying the correctness of wo...The correctness of workflow models is one of the major challenges in context of workflow analysis. The aim of this paper is to provide an improved Petri net-based reduction approach for verifying the correctness of workflow models. To the end, how to represent well-behaved building blocks and control structures of business processes by Petri nets is given at first, and then how to build well-structured process nets is presented. According to the structural characteristics of well-structured process nets, a set of legacy reduction rules are improved and extended, and then a complete Petri-net-based verification approach is proposed. The sound ness and the complexity with polynomial time for the improved re duction method are also proven.展开更多
The effect of social network structure on team performance is difficult to investigate using standard field observational studies. This is because social network structure is an endogeneous variable, in that prior tea...The effect of social network structure on team performance is difficult to investigate using standard field observational studies. This is because social network structure is an endogeneous variable, in that prior team performance can influence the values of structural measures such as centrality and connectedness. In this work we propose a novel simulation model based on agent-based modeling that allows social network structure to be treated as an exogeneous variable but still be allowed to evolve over time. The simulation model consists of experiments with multiple runs in each experiment. The social network amongst the agents is allowed to evolve between runs based on past performance. However, within each run, the social network is treated as an exogenous variable where it directly affects workflow performance. The simulation model we describe has several inputs and parameters that increase its validity, including a realistic workflow management depiction and real-world cognitive strategies by the agents.展开更多
Nowadays an increasing number of workflow products and research prototypes begin to adopt XML for representing workflow models owing to its easy use and well understanding for people and machines. However, most of wor...Nowadays an increasing number of workflow products and research prototypes begin to adopt XML for representing workflow models owing to its easy use and well understanding for people and machines. However, most of workflow products and research prototypes provide the few supports for the verification of XML-based workflow model, such as free-deadlock properties, which is essential to successful application of workflow technology. In this paper, we tackle this problem by mapping the XML-based workflow model into Petri-net, a kind of well-known formalism for modeling, analyzing and verifying system. As a result, the XML-based workflow model can be automatically verified with the help of general Petri-net tools, such as DANAMICS. The presented approach not only enables end users to represent workflow model with XML-based modeling language, but also the correctness of model can be ensured, thus satisfying the needs of business processes.展开更多
In order to effectively control the random tasks submitted and executed in grid workflow,a grid workflow model based on hybrid petri-net is presented. This model is composed of random petri-net,colored petri-net and g...In order to effectively control the random tasks submitted and executed in grid workflow,a grid workflow model based on hybrid petri-net is presented. This model is composed of random petri-net,colored petri-net and general petri-net. Therein random petri-net declares the relationship between the number of grid users' random tasks and the size of service window and computes the server intensity of grid system. Colored petri-net sets different color for places with grid services and provides the valid interfaces for grid resource allocation and task scheduling. The experiment indicated that the model presented in this letter could compute the valve between the number of users' random tasks and the size of grid service window in grid workflow management system.展开更多
工作流系统成功的关键在于向其输入的工作流的质量,因此工作流的建模就显得非常重要。工作流网(WF-net)是由 Petri 网发展起来的一种适用于多种系统的图形化、数学化建模工具。首先它有精确的定义,其次这种形式化体系可以用来反思过程,...工作流系统成功的关键在于向其输入的工作流的质量,因此工作流的建模就显得非常重要。工作流网(WF-net)是由 Petri 网发展起来的一种适用于多种系统的图形化、数学化建模工具。首先它有精确的定义,其次这种形式化体系可以用来反思过程,所以它是一种严格的过程形式化体系。讨论 WF-net 的建模技术,并以办公自动化系统中收文为例说明其应用,并分析其在众多的建模工具中所具有的优势。展开更多
基金supported in part by the National Key R&D Program of China(2017YFB1001804)Shanghai Science and Technology Innovation Action Plan Project(16511100900)the National Natural Science Foundation of China(61572360)
文摘Consistency degree calculation is established on the basis of known correspondence, but in real life, the correspondence is generally unknown, so how to calculate consistency of two models under unknown correspondence has become a problem. For this condition, we should analyze unknown correspondence due to the influence of different correspondences.In this paper we obtain the relations of transitions based on event relations using branching processes, and build a behavioral matrix of relations. Based on the permutation of behavioral matrix, we express different correspondences, and define a new formula to compute the maximal consistency degree of two workflow nets. Additionally, this paper utilizes an example to show these definitions, computation as well as the advantages.
基金Supported by the National Natural Science Foun-dation of China (60573046)
文摘The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic （CTL） allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic ＊ （CTL ＊ ） can be used to character the relaxed soundness of the workflow.
基金supported by the National Natural Science Foundation of China(61873030,62002019).
文摘In a cloud-native era,the Kubernetes-based workflow engine enables workflow containerized execution through the inherent abilities of Kubernetes.However,when encountering continuous workflow requests and unexpected resource request spikes,the engine is limited to the current workflow load information for resource allocation,which lacks the agility and predictability of resource allocation,resulting in over and underprovisioning resources.This mechanism seriously hinders workflow execution efficiency and leads to high resource waste.To overcome these drawbacks,we propose an adaptive resource allocation scheme named adaptive resource allocation scheme(ARAS)for the Kubernetes-based workflow engines.Considering potential future workflow task requests within the current task pod’s lifecycle,the ARAS uses a resource scaling strategy to allocate resources in response to high-concurrency workflow scenarios.The ARAS offers resource discovery,resource evaluation,and allocation functionalities and serves as a key component for our tailored workflow engine(KubeAdaptor).By integrating the ARAS into KubeAdaptor for workflow containerized execution,we demonstrate the practical abilities of KubeAdaptor and the advantages of our ARAS.Compared with the baseline algorithm,experimental evaluation under three distinct workflow arrival patterns shows that ARAS gains time-saving of 9.8% to 40.92% in the average total duration of all workflows,time-saving of 26.4% to 79.86% in the average duration of individual workflow,and an increase of 1% to 16% in centrol processing unit(CPU)and memory resource usage rate.
文摘In this paper, we propose astochastic Petri net model P-timed Workflow (WPTSPN) to specify, verify, and analyze a business process (BP) of a Flexible Manufacturing System (FMS). After formalizing the semantics of our model, we illustrate how to verifysome of its properties (reachability, safety, boundedness, liveness, correctness, alive tokens, and security) in the P-Timed context. Next, we validate the relevance of the proposed model with MATLAB simulation through a specific FMS case study. Finally, we use a generalized truncated density function to predict the duration of a token’s sojourn (residence) in a timed place with respect to the sequence states of the global FMS workflow.
文摘Access control is an important protection mechanism for information systems. This paper shows how to make access control in workflow system. We give a workflow access control model (WACM) based on several current access control models. The model supports roles assignment and dynamic authorization. The paper defines the workflow using Petri net. It firstly gives the definition and description of the workflow, and then analyzes the architecture of the workflow access control model (WACM). Finally, an example of an e-commerce workflow access control model is discussed in detail.
基金Project supported by the National Science and Technology Major Project of China (No.2010ZX01042-002-002-01)the National Basic Research Program (973) of China (No.2009CB320700)the National Natural Science Foundation of China (Nos.61073005 and 61003099)
文摘Workflow management is concerned with automated support for business processes.Workflow management systems are driven by process models specifying the tasks that need to be executed,the order in which they can be executed,which resources are authorised to perform which tasks,and data that is required for,and produced by,these tasks.As workflow instances may run over a sustained period of time,it is important that workflow specifications be checked before they are deployed.Workflow verification is usually concerned with control-flow dependencies only;however,transition conditions based on data may further restrict possible choices between tasks.In this paper we extend workflow nets where transitions have concrete conditions associated with them,called WTC-nets.We then demonstrate that we can determine which execution paths of a WTC-net that are possible according to the control-flow dependencies,are actually possible when considering the conditions based on data.Thus,we are able to more accurately determine at design time whether a workflow net with transition conditions is sound.
基金Supported by the Scientific Research Foundation of Edu-cation Agency of Liaoning Province (20040088) and Scientific ResearchFoundation of Dalian Nationalities University (20046202)
文摘The correctness of workflow models is one of the major challenges in context of workflow analysis. The aim of this paper is to provide an improved Petri net-based reduction approach for verifying the correctness of workflow models. To the end, how to represent well-behaved building blocks and control structures of business processes by Petri nets is given at first, and then how to build well-structured process nets is presented. According to the structural characteristics of well-structured process nets, a set of legacy reduction rules are improved and extended, and then a complete Petri-net-based verification approach is proposed. The sound ness and the complexity with polynomial time for the improved re duction method are also proven.
文摘The effect of social network structure on team performance is difficult to investigate using standard field observational studies. This is because social network structure is an endogeneous variable, in that prior team performance can influence the values of structural measures such as centrality and connectedness. In this work we propose a novel simulation model based on agent-based modeling that allows social network structure to be treated as an exogeneous variable but still be allowed to evolve over time. The simulation model consists of experiments with multiple runs in each experiment. The social network amongst the agents is allowed to evolve between runs based on past performance. However, within each run, the social network is treated as an exogenous variable where it directly affects workflow performance. The simulation model we describe has several inputs and parameters that increase its validity, including a realistic workflow management depiction and real-world cognitive strategies by the agents.
文摘Nowadays an increasing number of workflow products and research prototypes begin to adopt XML for representing workflow models owing to its easy use and well understanding for people and machines. However, most of workflow products and research prototypes provide the few supports for the verification of XML-based workflow model, such as free-deadlock properties, which is essential to successful application of workflow technology. In this paper, we tackle this problem by mapping the XML-based workflow model into Petri-net, a kind of well-known formalism for modeling, analyzing and verifying system. As a result, the XML-based workflow model can be automatically verified with the help of general Petri-net tools, such as DANAMICS. The presented approach not only enables end users to represent workflow model with XML-based modeling language, but also the correctness of model can be ensured, thus satisfying the needs of business processes.
基金the National Natural Science Foundation of China (No.60573141, 70271050)the Natural Science Foundation of Jiangsu Province (No.BK2005146)+3 种基金the High Technology Research Programme of Jiangsu Prov-ince (No.BG2005037, BG2005038, BG2006001)the High Technology Research Programme of Nanjing (No. 2006RZ105)the Foundation of National Laboratory for Modern Communications (No.9140C1101010603)the Key Laboratory of Information Technology Processing of Jiangsu Province (No.kjs05001, kjs0606).
文摘In order to effectively control the random tasks submitted and executed in grid workflow,a grid workflow model based on hybrid petri-net is presented. This model is composed of random petri-net,colored petri-net and general petri-net. Therein random petri-net declares the relationship between the number of grid users' random tasks and the size of service window and computes the server intensity of grid system. Colored petri-net sets different color for places with grid services and provides the valid interfaces for grid resource allocation and task scheduling. The experiment indicated that the model presented in this letter could compute the valve between the number of users' random tasks and the size of grid service window in grid workflow management system.
文摘工作流系统成功的关键在于向其输入的工作流的质量,因此工作流的建模就显得非常重要。工作流网(WF-net)是由 Petri 网发展起来的一种适用于多种系统的图形化、数学化建模工具。首先它有精确的定义,其次这种形式化体系可以用来反思过程,所以它是一种严格的过程形式化体系。讨论 WF-net 的建模技术,并以办公自动化系统中收文为例说明其应用,并分析其在众多的建模工具中所具有的优势。
