In our previous work, we considered, on the one hand, the predicate-based unfolding of a business process's conditional control flow and, on the other hand, the introduction of assertions for the contents of messages exchanged between processes. In this paper, we will sketch how both approaches can be smoothly combined for the automated provisioning of precise low-level Petri net models of business processes.
The quality of Petri-net-based verification of business processes is tightly coupled to the precision of the process model used. In particular, if verification targets the soundness or controllability of full-specified processes, i.e., executable BPMN or WS-BPEL processes, the Petri net model of a process must reflect the process’s control flow as well as process data relevant to the control flow. Otherwise, a thus imprecise process model comprises the danger of an erroneous verification. Yet, a precise and verifiable Petri net model can not be given in the general case due to the Turing-completeness of languages BPMN and WS-BPEL.
In our previous work [
In this paper, in order to widen the range of cases our methods are successfully
applicable, we integrate the individual methods, namely predicate-based
controllfow unfolding [
Discount $discount := $value * 0.01 $discount > 0 Receive
Account
Add Discount otherwise
No Discount $value > 500 Calculate
Discount otherwise
No Discount
Send
Discount $discount := 0 $discount := $value * 0.01 $discount := 0
In principle, predicate-based control-flow unfolding [
Figure 1 a) gives an example: It shows a snippet of a business process, in which the discount for a customer’s order is calculated ($discount), sent to the customer, and booked to the customer’s account if greater than zero. In Figure 1 b), the result of unfolding the snippet is shown. While unfolding, abstractions $discount > 5 and $discount = 0 were automatically derived for $discount’s value using static analysis and assigned individual control flow paths. Thereupon, the data-based choice with condition $discount > 0 could be successfully evaluated and resolved based on the abstract values. 3
However, mapping the unfolded snippet in Figure 1 b) to a Petri net, using the
Petri net semantics of [
In [
content and P a first-order predicate. As a remark, this definition can be easily extended to messages containing multiple data items and to assertions with formulas over more than one predicate. Doing so in particular allows for reusing the predicate-based abstraction for process data, which has been derived and utilized in the process of unfolding, as assertions for (outgoing) messages.
For the example in Figure 1 b), message channels with assertions ∀x: (x > 5) and ∀x: (x = 0) are introduced for outgoing message Discount. Consequently, mapping the snippet to a Petri net now yields a precise process model (Figure 2), such that a partner is enabled to determine whether it is expected to send another message or not by considering the assertions assigned to message Discount.
Since existing Petri net models for (distributed) business processes do not
support assertions for message contents, we need to extend their communication
model. For open workflow nets [
Existing approaches for mapping business processes to Petri nets either omit
process data entirely or restrict themselves to finite data [
In this paper, we have sketched the smooth integration of our previously introduced methods into a consolidated technique by way of an example. Using the technique then allows for generating more precise Petri-net-based process models for business processes in a significant number of cases. In particular, applying the technique to a set of problematic patterns of distributed processes, supplied by an industrial partner (see Appendix A), revealed the successful generation of precise process models for six out of ten process patterns. However, the thorough assessment of eficacy remains subject to future work. To this end, we plan to evaluate the consolidated technique using our process-to-Petri-net compiler.
$v:=true else $v=true message B
Reply B message A
$v:=false
$v:=1
else $v>0 $v:=Receive A Reply A
$v:=Receive A
$v:=12
else $v>0 $v:=$v−1
$v>0 $v:=$v−1
Pattern 4 (solved) $v:=0 $a:=(−1) else $v>$a $v:=$a $a:=Receive A
$v:=0 $v:=v+1
message A message B message A message B
Receive B $a:=Receive A $b:=Receive B $v:=0
$v:=1 Reply B $v:=$a Reply A $v:=$b Reply B $v>0 else $v>0 else
Receive D Receive C Receive D message A message B message C message D $a:=Receive A $b:=Receive B $c:=Receive C $d:=Receive D $x:=$a $x:=$b $x:=$c $x:=$d $c:=Receive C $d:=Receive D $d:=Receive D $c:=Receive C $y:=$c $y:=$d $y:=$d $y:=$c else else