In this work we propose a visual language for specifying behavioral properties of business processes (BP). We use Business process modeling notation (BPMN) to modelize BP, Petri Net as underlying formal foundations, and SPIN model checker to validate the dynamic behaviors of this process. The objective of this paper is to propose graphical property specification language which can be used during the design phase of BP. The proposed visual language uses the same concepts as established in BPMN to specify the properties to be verified. A semantic interpretation for properties expressed is given based en temporal logic formulas. The advantage of the proposed language is that it hides the temporal logic used for the specification of properties, and the knowledge of this logic is not needed.
In recent years, researchers have become
increasingly interested in developing methods and tools
for the specification and validation of Business
Processes (BP) behavior. The Business Process
Modeling Notation BPMN OMG (2011) is emerging as a
widely accepted approach in the domain of Business
Process Mana
Van der Aalst and Van Dongen (2013); Fahland et al. (2011). Most of these approaches are based on the mapping of BPMN to a formal presentation like Petri Net Murata and Koh (1989); El Hichami et al. (2014), YAWL Sun et al. (2008), PROMELA1, and PNML Hillah et al. (2010), in order to use the formal analysis tools available for these models. When model-cheking is considered for formally verifying BP properties, the specifications of this properties should be expressed by temporal logic formulas. Temporal properties are not always easy to write or read and need strong background knowledge. The objective of this paper is to propose a userfriendly graphical interface that business experts can use to specify and verify business processes. Furthermore, this approach allows the integration of formal verification techniques of BPMN models in the design phase.
The intent of this paper is to collect properties
(patterns) that occur commonly in the specification
of BP. Most specification formalisms in this domain
are a bit tricky to use. To make them easier to use,
our patterns use the same concepts as established
1spinroot.com/spin/Man/promela.html
in BPMN and come with descriptions that illustrate
how to map well-understood conceptions of BP
behavior into precise statements in common formal
specification languages like linear temporal logic
(LTL) MANNA and PNUELI (1992) and computation
tree logic (CTL)
Current research in this area are largely
concentrated on a translation of BPMN models to a formal
language, and the specification of the proprieties
is written in temporal logic, and does not consider
a visual language for specifying these proprieties
to be ve
In this section, we give the basic definitions, notations of BPMN, and Petri Net used in this paper. 3.1. BPMN BPMN is a graphical notation designed for both business process design and business process implementation. BPMN process models are composed of: 1. Events: (a) Start Event: it indicates where a particular process will start; (b) End Event: it indicates where a process will end. 2. Task: is a generic type of work to be done during the course of a BP. 3. Sequence flow: it links two objects in a process diagram. 4. Gateways: (a) And-split Gateway: is where a single branch is divided into two or more parallel branches which are executed concurrently; (b) And-join Gateway: is where two or more different branches of the process merge into one single branch; (c) Or-split Gateway: it routes the sequence flow to exactly one of the outgoing branches based on conditions; (d) Or-join Gateway: it awaits one incoming branch to complete before triggering the outgoing flow.
Fig. 1 provides an overview of a subset of BPMN
elements related to control-flow specification, these
include sequence flows. An object can be an event,
activity or gateway. A sequence flow links two objects
in a process diagram and denotes a control flow
relation.
3.1.1. Example
For further clarification, we give a simple example
adapted f
Petri Net is widely used tool for the representation,
validation and verification of BP Van der Aalst (1997,
1998); Ba
T ) [ (T
P ) is the flow relation.
A place can contain zero or more tokens. A token is represented by a black dot. The global state of a Petri Net, also called a marking, is the distribution of tokens over places. Formally, a marking of a Petri Net N is a function M : P ! N. The initial marking of N is denoted by M0.
An example of Petri Net is shown in Fig. 4.
3.3. Transforming BPMN models to Petri Net
In order to analyze formally BPMN models, several
transformations have been proposed Lohmann et al.
(2009);
The Petri net, representing the recuitment process
of Fig. 2, that is produced by applying the mapping
rules mentioned above is given in Fig. 4.
4. A VISUAL LANGUAGE FOR BP PROPERTY
SPECIFICATION (BPVSL)
In this section, we show how the designer can
specify the properties to be verified using a
graphical interface based on the same concepts
as established in BPMN. The framework uses
this specification as a guide to implement the
transformation to LTL MANNA and PNUELI (1992)
or CTL
Before illustrating the BPVSL that we propose, we give the set of properties that may be needed by the designer:
Safety property: that “nothing bad” will happen, ever, during the execution of a system like the absence of dead transitions (deadlocks).
Liveness property: that “something good” will happen, eventually, during the execution of a system like the absence of cyclical behaviors. Fairness property: under certain conditions, an event may occur repeatedly, is a special type of a safety property.
Invariant property: is a special case of a safety property. This type of property is satisfied with all system states.
Response property: if action A occurs then eventually action B will occur.
To specify the dynamic behavior of a BP, five models of response properties (Fig. 5) are considered in our BP Visual Specification Language (BPVSL). The following sections provide some of the most frequently interpretation of this patterns. The designer can use a graphical interface to specify the source and the target extremities of property to be verified. Then, the framework proposes the collection of the gateways and arrow types in order to choose the desirable semantic.
Temporal logic as extension of boolean logic may be used as formal language to express the properties that must be satisfied by the runs of a BPMN model. LTL is the logic we use in this paper.
The syntax of LTL is inductively defined as: ::= pj:j j ^ j _ j ! j j j j U . Such p is a atomic proposition (task in BPMN). The intuitive meanings of the associated LTL formulas are given below: : means
is true in next state; : means
is true in some future state; : means
is true in all future states; 1U 2: means until 2 holds.
1 is true in all future states
The syntax of CTL is inductively defined as: ::= pj:j j ^ j _ j ! .
Thus, in addition to introducing temporal operators, it introduces for-all and existential quantifiers: A : means has to hold in every future state on every execution path; E : means has to hold in every future state on some execution path; A : means has to hold in some future state in every execution path; E : means has to hold in some future state in some execution path.
For more details see MANNA and PNUELI (1992);
Every time ti is executed, tj and tk have to be executed in parallel afterwards: (ti ) ( tj ^ tk)), (LTL formula).
When ti is executed, tj and tk have to be executed afterwards, while the two outgoing branches are activated in parallel, each branch on all potential paths: (ti ) (A tj ^ A tk)), (CTL formula).
Every time ti is executed, tj and tk have to be executed in parallel afterwards: (ti ) ( tj ^ tk)), (LTL formula). 4.6. Specification language and semantic of 3 Every time ti is executed, one of the tasks ti or tk has to be executed afterwards: (ti ) ( tj _ tk)), (LTL formula).
One of the tasks tj or tk eventually is executed after the task ti on each potential path: (ti ) (A tj _ A tk)), (CTL formula).
Every time ti is executed, one of the tasks ti or tk has to be executed afterwards: (ti ) ( tj _ tk)), (LTL formula). 4.7. Specification language and semantic of 4
Formal semantics
4: Every time tasks ti and tj are simultaneously executed, tk has to be executed afterwards: ((ti ^ tj ) ) tk), (LTL formula).
When merging parallel branches, outgoing branch on all potential paths: ((ti^tj ) ) A tk), (CTL formula).
Every time tasks ti and tj are simultaneously executed, tk has to be executed afterwards: ((ti ^ tj ) ) tk), (LTL formula). 4.8. Specification language and semantic of 5
One of the tasks ti or tj will be eventually followed by the task tk on each potential path: ((ti _ tj ) ) A tk), (CTL formula).
Every time one of the tasks ti or tj is executed, it is followed by the task tk: ((ti _ tj ) ) tk), (LTL formula).
In order to meet the requirements of the designer, we propose to add for each property to be verified a sets of properties in order to define safety, liveness, invariant and fairness properties. 4.9.1. A safety property are conditions that are verified along any execution path. These type of properties are usually associated with some critical behaviour, thereby they should always hold. Then, the quantifier ( ) is good for the safety property. For example, in the case of BPMN model of the recruitment process, the company never recruits a “bad candidate”. 4.9.2. A liveness property These type of properties involved in the temporal concept with eventually. Thus, the quantifier ( ) is good for the liveness property. Practically, in the case of BPMN model of the recruitment process, never reach the “good candidate”. 5. VERIFICATION PROCESS AND CASE STUDY The verification process proposed of BP (Fig. 11), the designer uses a graphical interface to modelize the BPMN and to specify the desired properties to be verified using BPVSL. The framework uses this specification as a guide to implement the transformation to corresponding LTL temporal logic. As examples, we show how to specify three response properties using BPVSL.
Example 1: We could use the specification language semantics of 1 to specify the following property ( 1): Does the task “Setup payroll” will happen after the tasks “Find candidates” This property can be interpreted with the visual presentation of Fig. 12. When the source extremity of 1 is selected, the framework proposes only the reachable tasks as target extremities of 1. Then, the designer can specify the arrow types between the task “Find candidates” and “Setup payroll”. Example 2: Let 2 be the property given by: the task “Study CVs” and task “Evaluate interviews” will be executed in parallel and after task “Receive candidate CVs”. This property can be interpreted with the visual presentation of Fig. 13. In fact, the designer has first to select a task “Receive candidate CVs”, then the designer has to select only the reachable tasks “Study CVs” to be executed in parallel with the task “Evaluate interviews” as the target extremities of 2. Finally, the framework proposes the collection of the gateways and arrow types in order to choose between the different semantics of 2. Example 3: Let 3 be the property given by: Task “Find candidates” will be executed after the tasks “CV not approved” or “Not successful interviews”. This property can be interpreted with the visual presentation of Fig. 14. Similar to the specification of 1 and 2, when the first source extremity “CV not approved” of 3 is selected, the designer selects the task “CV not approved” as the second source extremity of 3 to be executed in conditional with the task “CV not approved”, and the reachable task “Find candidates” as the target extremity of 3. Finally, the designer can choose between the collection of the gateways and arrow types.
In this paper, we use the SPIN tools3 to validate the LTL formulas. In these experiments, we discuss the verification of three models of response properties 1, 2 and 3 of Section 5. 6.1. Transforming Petri Net to PROMELA In order to simulate Petri Net using SPIN, it is necessary to translate Petri Net models into SPIN models-specified using PROMELA.
In Holzmann (2003), the authors propose a method to describe a Petri Net into PROMELA that can be simulated and verified with the SPIN model checker. In this method, a Petri Net system is represented 3http://spinroot.com/spin/Man/ as a single process. The process describes each firing of its transitions. An outline of the PROMELA program of the Petri Net corresponding to the recruitment process is given bellow: #define Place 25 #define Transition 25 int M[Place]; /* Marking */ int X[Transition]; /* Firing count */ /* A firing of Transition t*/ /* remove specifies the change of the marking of preset of t */ /* add specifies the change of the marking of postset of t */ /* fire (x) increments the element
corresponding to t in X[t] */ #define remove1(x) (x>0) -> x-#define remove2(x,y) (x>0 && y>0) -> x--; y-#define add1(x) x++ #define add2(x,y) x++; y++ #define fire(x) x++ /* Process representing Petri Net */ init { M[0]=1; /* Set the initial marking */ do :: atomic{remove1(M[0]) -> fire(X[0]); add1(M[1]} :: atomic{remove1(M[1]) -> fire(X[1]); add1(M[2]} :: atomic{remove1(M[2]) -> fire(X[2]); add1(M[3]} :: atomic{remove1(M[3]) -> fire(X[3]); add1(M[4]} :: atomic{remove1(M[4]) -> fire(X[4]); add1(M[5]} :: atomic{remove1(M[5]) -> fire(X[5]); add1(M[6]} :: atomic{remove1(M[6]) -> fire(X[6]); add2(M[7], M[12])} :: atomic{remove1(M[7]) -> fire(X[7]); add1(M[8]} :: atomic{remove1(M[8]) -> fire(X[8]); add1(M[9]} :: atomic{remove1(M[8]) -> fire(X[8]); add1(M[17]} :: atomic{remove1(M[9]) -> fire(X[9]); add1(M[10]} :: atomic{remove1(M[10]) -> fire(X[10]); add1(M[11]} :: atomic{remove1(M[11]) -> fire(X[11]); add1(M[5]} :: atomic{remove1(M[12]) -> fire(X[12]); add1(M[13]} :: atomic{remove1(M[13]) -> fire(X[13]); add1(M[14]} :: atomic{remove1(M[13]) -> fire(X[13]);
add1(M[19]} :: atomic{remove1(M[14]) -> fire(X[14]); add1(M[15]} :: atomic{remove1(M[15]) -> fire(X[15]); add1(M[16]} :: atomic{remove1(M[16]) -> fire(X[16]); add1(M[5]} :: atomic{remove1(M[9]) -> fire(X[17]); add1(M[17]} :: atomic{remove1(M[17]) -> fire(X[18]); add1(M[18]} :: atomic{remove1(M[14]) -> fire(X[19]); add1(M[19]} :: atomic{remove1(M[19]) -> fire(X[20]); add1(M[20]} :: atomic{remove2(M[18],M[20]) ->
fire(X[21]); add1(M[21])} :: atomic{remove1(M[21]) -> fire(X[22]); add1(M[22]} :: atomic{remove1(M[22]) -> fire(X[23]); add1(M[23]} :: atomic{remove1(M[23]) -> fire(X[24]); add1(M[24]} od } (The PROMELA description of Petri Net shown in Fig. 4)
The properties to be verified in SPIN have to be expressed as LTL formulas. LTL formulas corresponding to to the response properties 1, 2 and 3 to be verified can be rewritten as follows: 1: Does the task “Setup payroll” will happen after the tasks “Find candidates” ; LTL formula: [ ]((M [5] >= 1) > <> (M [21] >= 1));
2: Task “Study CVs” and task “Evaluate interviews” will be executed in parallel and after task “Receive candidate CVs” ; LTL formula: [ ]((M [3] >= 1) > <> (M [12] >= 1 && M [8] >= 1));
3: Task “Find candidates” will be executed after the tasks “CV not approved” or “Not successful interviews”.
LTL formula: [ ]((M [15] >= 1 j j M [10] >= 1) > <> (M [5] >= 1)).
In this section, we give some statistics in order to show the performance of our approach. We present the size, the memory and the verification time of the verification of 1, 2 and 3 on the Petri Net related to Fig. 4.
We first investigated in Table 1 and Table 2 the results without Safety properties and with Liveness properties.
In Table 3 we present the results with Safety properties(invalid deadlock) and without Liveness properties.
The paper proposes a visual language for specifying business process behavior. We use BPMN to modelize BP, Petri Net as underlying formal foundations, and spin model checker to perform automated analysis. The principal objective of this paper is to propose a graphical framework which use the same notation as established in BPMN. In this way the designer can specify and validate the BP properties during the design phase. Several formal semantics for these properties are expressed as temporal logic formulas. Times (s) Mohammed AbuJarour and Ahmed Awad. (2014) Web Services and Business Processes: A Round Trip. Web Services Foundations : pp. 3-29. OMG. (2011) Business Process Modeling Notation (BPMN) Version 2.0. OMG Final Adopted Specification. Object Management Group.
T. Takemura. (2008) Formal semantics and verification of BPMN transaction and compensation. In Proc. of APSCC 2008, pp. 284-290. IEEE. J. W. Bryans, J. S. Fitzgerald, A. Romanovsky, and A. Roth. (2009) Formal modelling and analysis of business information applications with fault tolerant middleware. In Proc. of ICECCS 2009, pp. 68-77. IEEE Computer Society.
O. El Hichami, M. Al Achhab, I. Berrada and B.
El Mohajir. Graphical specification and automatic verification of business process, the International Conference on Networked systems. NETYS 2014, LNCS 8593, Springer, pp. 1-6.
W.M.P. van der Aalst and B.F. van Dongen. (2013) Discovering Petri Nets From Event Logs. T. Petri Nets and Other Models of Concurrency 7: 372422.
Dirk Fahland, Cdric Favre, Jana Koehler, Niels Lohmann, Hagen Volzer, Karsten Wolf. (2011) Analysis on demand: Instantaneous soundness checking of industrial business process models.
Data Knowl. Eng. 70(5): pp.448-466.
T. Murata and J.Y. Koh (1989) Petri nets: Properties, Analysis and Applications. an invited surve y paper, Proceedings of the IEEE, Vol.77, No.4 pp.541-580.
O. El Hichami, M. Al Achhab, I. Berrada, R. Oucheikh and B. El Mohajir. (2014) An Approach Of Optimisation And Formal Verification Of Workflow Petri Nets. Journal of Theoretical and Applied Information Technology, Vol.61, No.3 pp. 486-495. J.-H. Ye, S.-X. Sun, L. Wen, and W. Song. (2008) Transformation of BPMN to YAWL. In CSSE (2), pp. 354-359. IEEE Computer Society.
L. Hillah, F. Kordon, L. Petrucci, and N. Trves. (2010) PNML Framework: an extendable reference implementation of the Petri Net Markup Language, LNCS 6128, pp. 318–327.