发明名称 Computer-implemented method, computer program product and system for analyzing a control-flow in a business process model
摘要 A new technique to analyze the control-flow, i.e., the workflow graph of a business process model, which is called symbolic execution, is provided. Acyclic workflow graphs that may contain inclusive OR-gateways are considered; a symbolic execution for them is defined, which runs in quadratic time. In particular, this symbolic execution essentially comprises labeling edges of nodes of the graph such that a label assigned to a first edge comprises a set of one or more edge identifiers, each identifying a second edge that is an outgoing edge of an XOR-split or an IOR-split node in the graph, whereby executing the second edge ensures that the first edge will be executed. Such a scheme may permit a decision for any pair of control-flow edges or tasks of the workflow graph whether they are sometimes, never, or always reached concurrently. This has different applications in finding control- and data-flow errors.
申请公布号 US9477937(B2) 申请公布日期 2016.10.25
申请号 US201313755949 申请日期 2013.01.31
申请人 INTERNATIONAL BUSINESS MACHINES CORPORATION 发明人 Favre Cedric;Voelzer Hagen
分类号 G06Q10/04;G06Q10/06 主分类号 G06Q10/04
代理机构 Tutunjian & Bitetto, P.C. 代理人 Tutunjian & Bitetto, P.C. ;Davis Jennifer R.
主权项 1. A computer program residing on a non-transitory computer-readable storage medium, comprising instructions for causing a computer system to implement steps for analyzing a control-flow in a business process, the steps comprising: invoking a representation of the business process as an acyclic workflow graph containing AND-, XOR- and IOR-types of nodes and edges linking nodes of the graph; labeling edges of the graph such that a label assigned to a labeled edge comprises a plurality of edge identifiers identifying respective edges, each of the edges identified being an outgoing edge of an XOR-split or an IOR-split node in the graph, whereby executing any one of the identified edges ensures that the labeled edge will be executed; and automatically checking the labels for a deadlock using a processor, while labeling the edges of the graph, wherein a deadlock is found if a condition for relaxed soundness is true.
地址 Armonk NY US