In our previous work, we have introduced a technique to unfold the control flow in workflow graphs based upon static information about constant data values. Using this technique allowed us to safely transform certain kinds of conditional into unconditional control flow, and thus to support a usually data-unaware verification of business processes by more accurate process models. In this paper, a generalisation of this technique is discussed which can be employed in combination with arbitrary information about data values. This way, we show how statically derived value range information is beneficial for unfolding and therefore eliminating conditional control flow in a wider range of cases.
Verification of business processes today is often done using a Petri-net-based
process model in which data aspects are being neglected. Prominent examples
are the verification of soundness [
Given that properties like soundness or controllability relate to control flow,
this kind of wrong verification results is mainly due to an imprecise modelling
of business processes’ control flow. Reasoned by the ommitance of data aspects
within the Petri-net-based process model, conditional control flow is therein
overapproximated by nondeterminism, resulting in an abstraction too coarse. In [
The restructuring technique presented in [
else $balance1= 0
Acknowledge
Order at process runtime, separating and duplicating the control flow for each combination of assigned values then allows for the evaluation and substitution of the condition with unconditional control flow in each duplicate. Since the restructuring technique in its current form is thus restricted to analysis information about constant values, only conditions with variables defined over constants, or single messages, can be resolved. In this paper, we discuss a generalisation of the technique to relax this limitation. For that purpose, the generalised technique is enabled to be used in combination with an arbitrary static analysis which yields an abstraction for the values of process data. In particular, we will show how a value range analysis helps in resolving branching or loop conditions in cases condition variables are not necessarily restricted to constant values.
In principle, our restructuring technique can be seen as an unfolding of a process’s control flow. However, existing unfolding techniques restructure the entire process with all variables, though, it is only necessary to unfold those parts and variables related to a branching or loop condition. Further, unfolding at the value level is infeasible in case of infinite data domain such that an abstraction for variables’ values is required. Our restructuring approach overcomes these issues by guiding the control flow unfolding based on static analysis information.
The remainder of the paper is structured as follows: The next section introduces the process representation format and analysis used to derive value range information. In Section 3, we describe our generalised technique for guided control flow unfolding and its use in combination with value range information. Related work is discussed in Section 4. Finally, Section 5 concludes the paper. 2
In order to allow for the static derivation of information essential to our guided
control flow unfolding approach, a process representation format is required
which is capable of representing both, control as well as data aspects of a
business process. We therefore use an extension of workflow graphs [
Order Exit
Entry
InvalidOrder
Settlement
graphs support a simple and flexible modelling of a process’s control structure.
However, since workflow graphs only map control flow, we augment them with a
notation of process data. Thus, nodes and edges of a workflow graph are
annotated with data manipulation statements in Concurrent Static Single Assignment
(CSSA-)Form [
In Figure 1, an example process is shown in its representation as extended workflow graph (whose visualisation here closely follows the Business Process Model and Notation). The depicted process models the action of item exchange. A customer therein first specifies the item for exchange by sending message Claim. Afterwards, the customer is allowed to order exchange items via message Order, where each is acknowledged by message Acknowledgement, as long as the total value of orders does not exceed the value of the item for exchange. Otherwise, the last order is rejected, indicated via message InvalidOrder. In case the total value of ordered items eventually equals the value of the item for exchange, the claim is settled and message Settlement is sent to the customer.
For its realisation, the process is based on a loop whose execution is conditioned. In the Petri-net-based process model, as shown in Figure 2, the loop is mapped to the nondeterministic choice of transitions Entry and Exit, such that the loop condition is not precisely represented. In consequence, verifying the process using this Petri net model yields erroneous results for properties like controllability, e.g., the process is verified to be non-controllable although it is.
In contrast, the extended workflow graph explicitly models the loop condition: Loop execution is controlled by an integer variable $total2, representing the difference of the value of the item for exchange and the total value of all already ordered exchange items. Accordingly, if the value of the variable is greater than zero, the loop is executed, and otherwise exited. Therefore, the value of $total2 is initially set to the value of the item for exchange (message part $claim1.value), and afterwards updated for each loop iteration with the difference of its current value and the value of an accepted exchange item (message part $order1.value). As can be seen, all variables are statically only defined once, as is indicated by the variables’ subscripts. This is the main characteristic of CSSA-Form and vitally supports analysis since variables then coincide with their definition statements. Although, special handling is required if multiple variable definitions have to be joined at a single node of the extended workflow graph. In these cases, statements with so-called Φ-functions are used to merge the confluent definitions into a single value, as is done for the definitions of variables $total1 and $total4 by statement $total2 = Φ($total1,$total4).
To further improve analysis, the implications of branching and loop conditions are annotated in terms of assertion statements. For instance, since the loop in the example process is only executed if the value of variable $total2 exceeds zero, we know that the variable must be a positive integer within the body of the loop. Therefore, uses of $total2 in the loop body are substituted with a reference to a new variable which is defined by $total3 = assert($total2,$total2 > 0), indicating that $total3 equals $total2 and has a value greater than zero.
Based on the representation of business processes through extended workflow
graphs, various static analysis become available. In particular, the use of
CSSAForm facilitates the transfer of analysis techniques from the area of compiler
optimisation, like, e.g., constant propagation, global value numbering [
Value range analysis is a textbook data flow analysis technique which can be
used to derive an interval for each integer or floating-point variable and point of
a program, such that the variable is guaranteed to take a value in the interval
at the given program point. In [
An application of the analysis to the example process of Figure 1 yields the
value range information shown in Table 1. Note that, therein, each variable is
assigned a single interval which is valid at each point of the process, due to the
static single definition of variables in CSSA-Form. Further, the analysis defined
in [
assertion = assertion ∪ {variablecondition 7→ inf(variable)};
end for;
if (evaluate(guard, assertion) == true) then
let instance be the loop instance for assertion;
if (instance * eW F G) then eW F G = eW F G ∪ instance;
end if;
replace guard with a control flow edge to instance;
else replace guard with a control flow edge to the exit node of loop;
end if;
end while;
We now describe how the derived analysis information is used to guide control
flow unfolding in such a way that conditional control flow can be effectively
resolved. In our previous work [
In principle, unfolding a loop or branching so that conditional control flow is
transformed into unconditional control flow is done using two steps. First, the
loop or branching is converted into a normal form [
In Figure 3, a consolidated view of unfolding a loop is given in terms of an
algorithm. Therein, having derived static analysis information for a process’s
variables using function analyse, the loop is first converted into its normal form
as explained in [
Note that, in the algorithm, the use of analysis information is parameterised
using functions analyse and evaluate. Thus, it is possible to instantiate this
general algorithm for exploiting information provided by an arbitrary static analysis
by merely declaring implementations for functions analyse and evaluate, with
respect to the analysis. In case of our running example, function analyse denotes
the value range analysis as described in [
Claim
Order
InvalidOrder Settlement
An application of the algorithm to the loop contained in the example process of Figure 1 allows us to exploit the value range information given in Table 1 for unfolding the loop such that the loop condition is finally resolved. The thus unfolded workflow graph is shown in Figure 4. As can be seen, it was only necessary to create a single instance for assertion $total12 ∈ (0, +∞] while unfolding, where variable $total2 has therein been renamed to $total12.
In Figure 5, the unfolded workflow graph is mapped to a Petri net based on
the Petri net semantics for workflow graphs stated in [
In general, our technique provides in this way a heuristics for improving
verification in that the more conditional control flow is resolved, the more precise
is the Petri-net-based process model and therefore the verification. Furthermore,
if termination can be shown, e.g., using termination analysis [
Improving business process verification based on Petri nets by means of
incorporating data aspects is an ongoing research topic. In [
Control flow restructuring is also utilised by other program analysis and
optimisation methods for improving analysis results [
Main issue of future work will be the thorough evaluation of our process
restructuring technique. Therefore, we want to implement the technique for
structured business processes of the WS-BPEL language. As the value range analysis
has already been realised, we currently focus on the implementation of the
restructuring algorithm itself. Building on that, we further plan to employ other
static analysis, i.e., symbolic methods [