In a business process, control ow decisions are based on the evaluation of conditions. Thus, conditions must be considered for control ow veri cation. This paper shows how the Petri nets based control ow veri cation can be improved by analysing conditions and logical relations between them. We outline a Petri net extension with predicate transitions, which are responsible for conditions evaluation based on the collected knowledge, and e ect places, which contain fact tokens representing the e ects of certain operations and decisions made.
x > 100 x ≤ 100 if if y > 50 y ≤ 50 y := 20*x B D
As the complexity of business processes grows, the need for automatic veri cation becomes more important. We show an approach for veri cation for processes modelled with Petri nets. The properties to verify represent the constraints on possible execution traces. An example of such a constraint is \the payment must always be followed by a shipment", which can be expressed using LTL as G(P ayment ! F Shipment). To show that this constraint is ful lled, it must be proved that there is no possible execution path that contains a payment before a shipment (temporal dependency) and that there is no execution y := 10*x
A
C since the execution condition of C is implied by the execution condition of A and the fact that y becomes equal to 10 x if the left branch of the rst if is executed. Current Petri net based veri cation approaches abstract from the data and their relations and therefore make non-deterministic choice in both of the switch-constructs, which makes the phantom execution path (A; D) possible.
This paper shows how a Petri net can collect knowledge and use the collected knowledge to reason about the next step. Sect. 2 presents related work in this eld. The proposed extensions are shown in Sect. 3. Sect. 4 describes how the process knowledge is collected during the Petri net analysis and Sect. 5 shows how the collected knowledge is used for the predicate transitions evaluation. Sect. 6 demonstrates the analysis of the process fragment shown in Fig. 1 using the presented approach before Sect. 7 concludes. 2
A number of non-deterministic decisions take place during the analysis of a
Petri net: selection of a speci c if-branch, skipping or executing an activity, and
entering or exiting a loop. In the business process the decisions depend on the
evaluation of the corresponding conditions: branching condition, join condition,
loop condition. A join condition is a starting condition of a branch and is a
Boolean formula over the states of all incoming links [
An overview of existing BPEL formalizations and veri cation approaches is
provided in [
The conditions constrain the execution of the business process. In addition, the control ow decisions made in the past can in uence the decisions in the future, as the example of Fig. 1 illustrates: if the left branch of the rst if-activity is taken, then y is set to 10 x, where x > 100 according to the branch condition. This will in uence the branch selection of the second if-activity. This implies that the execution trace, which contains activity A and activity D, is impossible. It will, however, be considered as possible during the Petri net analysis if the data conditionSsawre nitecglecteEd. Sxutcehphasnitoomnexecution trace can only be detected if h n the relation between decisions leading to the execution of the activities A and D are known.
Each decision is bound to a certain condition. If a decision has to be made, the condition is evaluated and, depending on the evaluation result, a certain path in a work ow is chosen. During process runtime, the evaluation of the condition is simple, since instaCn1ce daif ta isCa2vailable. At design time, however, instance data is not available and thus only relations between process variables and between conditions can beA analysed. If a cBertain path in a work ow is chosen, then the condition of this path is true (e.g. x > y). Thus, even if we do not know the actual data, we know that the data relations captured in the path condition (e.g. x > y) are in force. We also say that the decision produces an e ect relations.
We add a predicate transition to decide whether a certain path can be executed. A predicate transition is responsible for the evaluation of the con- PT1 C1==true (¬ C1 ∧ C2)==true PT2 dition for a certain execution trace based on the collected knowledge. A decision transition is the transition D1 D2 responsible for selecting the actual execution trace from all possible execu- P1 C1 = true A B C2 = true P2 tion traces. A trace is considered to be an alternative if the corresponding condition was evaluated to true or un- Fig. 2. if activity in an extended Petri known by the predicate transition, see net Sect. 5. We record the e ect of the decision made by producing a token for an e ect place added after each red decision transition. This token means that the condition on this path is true and thus the relation represented by this condition is in force.
E ect places, predicate and decision transitions for an if -activity with two
branches are shown in Fig. 2. The predicate transitions P T1 and P T2 are
responsible for the evaluation of the branch conditions: C1 for the left and C2 for the
right branch. If the corresponding condition evaluates to true, the token will be
produced in the outgoing place, which in its turn will enable the selection of the
corresponding branch. If the condition evaluates to false, then the token from
the incoming place will be consumed and no token for the outgoing place will be
produced. Note, that the branch conditions are adjusted in such a manner that
only one of the conditions can simultaneously evaluate to true. This complies with
the if-activity execution semantic [
Li1, .J..Lin oin
Extension Where Lo1...Lok arTehoeutagtcoitivinvigittyylinhkassoaf join conditionFonig. 3. flow activity Li1
...
Join control flow
Lin PT3 JC(A)==true
JC(A)==false
PT4 P3 JC(A)=true
D3
Execute A
Skip A Split control flPowT3
...
Lo1 Lok (b) flow activity extended Petri net
D3 JC(A)==true D4
Li1 JC(A)=false P4
...
Join control flow
Lin thistoachtivointyloinrksthLei1f,a..c.tLitnh:aJtoibn(o1t.h..nb)ranch conditions can ePv3aluJaCt(Ae)=ttruoe unknown and thus Execute A the actual decision will be made by the decision transition.
For Feiagc.h3(joai)nschoonwdsitiaonn aadctdivaitryuleintoa BPEL flow. The activity has n incoming 9 linJkesnaanfdoradejoaidn pcaotnhdeitliimonindaetionne:d on the status of these links. Fig. 3(b) shows an extended Petri net for this activity. Here, the predicate transitions PSpTlit3control flow and P T4 are resJpooinns(i1b.l.e.nf)o-r>eLvoa1lu=atfiaolnseo,f the join condition, which helps tLho1e dec.i.si.on transitions .D..L3oakn=dfaDls4eto decide whether the activity A is to be executed or skipped. The extension required for loop constructs is similar to the if -activity WexhteernesiLoon1a..n.Ldoiks anroet osuhtogwoninignlitnhkiss poafper due to the space limitations. An assignactivity estatbhliisshaecstivreitlyations between process variables which are come in force after the activity has been executed. Therefore, an additional e ect place is added after the transition representing an assign activity. The next section presents how the produced e ects can be stored to enable reasoning on the colected knowledge. 4
The variable and condition relations currently in force are represented by the
tokens in the e ect places. The e ect places, and thus the knowledge about the
data relations, may either result from a decision e ect or from a relation between
process variables introduced by an assign activity. A decision e ect is a result of a
decision made for transition conditions, join conditions, if and pick branches. Let
C be the condition of the path selected by the decision transition. Then a new fact
C = true is added to the knowledge base. The relations between process variables
captured in the assign statements can also in uence decisions. For example, if an
assignment y := x + a was executed and it is known that a > 0, then it can be
derived that y > x. If an assign activity x := f (y1; : : : ; yn) is executed, then the
statement x = f (y1; : : : ; yn) becomes a fact and is added to the knowledge base.
Thereby, every occurrence of the same variable on the left side of assignment
gets a new index each time an assignment fact is added to the knowledge base.
If a variable occurs on the right side of the assignment, the variable with the
highest index currently available in the knowledge base is used. Note that this is
di erent to the CSSA approach [
PT4 D4
JC(A)=false P4 Skip A Lok 9 exclusive or concurrent read-write accesses to the same variable (expressed with the and -functions in CSSA). The reason for this is the step-by-step analysis considered in this paper, which implies that the knowledge base cannot contain contradictory information: only the relations captured in the assign statements on the chosen branch are added to the knowledge base and the order of the concurrent assignments is the one selected by the Petri net navigator. A receive, pick and invoke activity can be considered to contain an implicit assign of the message content to the process variables. 5
A predicate transition represents an invocation of a reasoner. A reasoner evaluates
the transition condition based on the current knowledge in the knowledge base.
This section shows how the evaluation of the condition can be reduced to the
satis ability problem. Let F1; : : : ; Fn be the current facts in the knowledge base,
let C be the condition to be evaluated. The condition evaluates to true if it
can be proved that C can be derived from the current facts in the knowledge
base. Formally speaking, the following must hold: F1; : : : ; Fn ` C. To prove
this, the following formula is checked for its satis ability: Vi2f1;:::;ng Fi ^ :C.
If this above formula is unsatis able, then C will always evaluate to true for
this execution path and therefore a token will be produced by the predicate
transition responsible for the evaluation of the condition C. If the above formula
is satis able, the following formula is checked: Vi2f1::ng Fi ^ C. If this formula
is unsatis able, then C will always evaluate to false for this execution path. In
this case the transition will not produce any token. If both formulas are satis able,
then the decision can only be made based on the concrete data and therefore both
cases should be considered for the analysis. In this case, the predicate transition
produces a token which will compete with other tokens. The actual decision will
be made non-deterministically by the decision transition in the same way as for
the non-extended Petri net: one of the tokens will be consumed, the others will
remain in their places and wait for the backtracking and selection/consumption
of the next token. The collected facts in the knowledge base represent the logical
relations between process variables currently in force. The satis ability of the
above formulas based on the current relations is checked using the Satis ability
Modulo Theories (SMT) solver Yices [
Petri net simulation – EPxaemtripnleet simulation – Example x>100 x≤100 x>100 Fig. 4. Analysis using knowledge base and a reasoner 16 18 in the e ect place x > 100 and the corresponding relation is added as a fact to the knowledge base. Fig. 4(c) shows the next invocation of the reasoner. There, the condition y > 50 evaluates to true and y 50 evaluates to false. Fig. 4(d) shows the status after the ring of the predicate transitions for the second if statement. The predicate transition of the right branch consumes the token on its input place, but does not produce an output token, since y 50 evaluates to false, while the predicate transition of the left branch produces an output token. Thus, only the left branch of second if activity is enabled.
This paper showed how a Petri net based veri cation of a business process can be enhanced by adding e ect places and predicate transitions. We showed how the conditions on the predicate transitions can be evaluated using the knowledge collected during the Petri net analysis. This enables resolving the nondeterministic decisions if the current decision strongly depends on the previously made decisions. Thus the \phantom" paths can be removed from the reachability graph which makes the analysis more e ective and precise.
The presented approach can also be used to analyze compositions of business processes, called choreographies. In this case, the knowledge base is shared by all processes and thus each process is aware of the constraints on the input data.
Our future work is to investigate the impacts of our work on current Petri
net reduction techniques. We are going to integrate the presented approach in
LoLA [