=Paper=
{{Paper
|id=Vol-1256/paper10
|storemode=property
|title=Visual Specification Language and Automatic Checking of Business Process
|pdfUrl=https://ceur-ws.org/Vol-1256/paper10.pdf
|volume=Vol-1256
|dblpUrl=https://dblp.org/rec/conf/vecos/HichamiABM14
}}
==Visual Specification Language and Automatic Checking of Business Process==
https://ceur-ws.org/Vol-1256/paper10.pdf
Visual Specification Language and Automatic Checking of Business Process 93
El Hichami • Al Achhab • Berrada • El Mohajir
Visual Specification Language and Automatic
Checking of Business Process
Outman El Hichami Mohammed Al Achhab Ismail Berrada
Faculty of Sciences, UAE, National School of Applied Sciences, Faculty of Sciences, USMBA,
Tetouan, Morocco Tetouan, Morocco Fez, Morocco
el.hichami.outman@taalim.ma alachhab@ieee.ma iberrada@univ-lr.fr
Badr Eddine El Mohajir
Faculty of Sciences, UAE,
Tetouan, Morocco
b.elmohajir@ieee.ma
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.
Business process, Model-checking, BPMN, Petri Net, Dynamic behavior
1. INTRODUCTION Van der Aalst and Van Dongen (2013); Fahland et
al. (2011). Most of these approaches are based on
In recent years, researchers have become increas- the mapping of BPMN to a formal presentation like
ingly interested in developing methods and tools Petri Net Murata and Koh (1989); El Hichami et al.
for the specification and validation of Business Pro- (2014), YAWL Sun et al. (2008), PROMELA1 , and
cesses (BP) behavior. The Business Process Mod- PNML Hillah et al. (2010), in order to use the formal
eling Notation BPMN OMG (2011) is emerging as a analysis tools available for these models. When
widely accepted approach in the domain of Business model-cheking is considered for formally verifying
Process Management Hofstede et al. (2003) and be- BP properties, the specifications of this properties
coming increasingly indispensable in business rela- should be expressed by temporal logic formulas.
tionship, web services AbuJarour and Awad (2014), Temporal properties are not always easy to write or
etc. BPMN is a standard and a well-known diagram- read and need strong background knowledge.
matic notation for supporting the specification of BP.
It provides symbols to a simple graphical specifi- The objective of this paper is to propose a user-
cation for defining the control flow of the business friendly graphical interface that business experts
process in the early phases of process development. can use to specify and verify business processes.
BPMN diagrams afford a notation that is readily Furthermore, this approach allows the integration of
understandable by all business users: the designer formal verification techniques of BPMN models in
expert, the technical developers, the business peo- the design phase.
ple who will manage and monitor these processes.
The intent of this paper is to collect properties
The mix of constructs found in BPMN and the lack of (patterns) that occur commonly in the specification
an unambiguous definition of some notations, makes of BP. Most specification formalisms in this domain
it possible to create models with semantic errors. are a bit tricky to use. To make them easier to use,
Therefore, several approaches have been proposed our patterns use the same concepts as established
to the formal validation of BPMN Takemura (2008); 1 spinroot.com/spin/Man/promela.html
Al Achhab et al. (2014); Bryans et al. (2009);
1
Visual Specification Language and Automatic Checking of Business Process 94
El Hichami • Al Achhab • Berrada • El Mohajir
in BPMN and come with descriptions that illustrate 3.1. BPMN
how to map well-understood conceptions of BP
behavior into precise statements in common formal BPMN is a graphical notation designed for both
specification languages like linear temporal logic business process design and business process im-
(LTL) MANNA and PNUELI (1992) and computation plementation. BPMN process models are composed
tree logic (CTL) Heljanko (1997). The rest of the of:
paper proceeds as follows: Section 2 discusses the
related work. Section 3 provides formal definitions 1. Events:
and notations of BPMN used in the rest of this (a) Start Event: it indicates where a particular
paper and the mapping from BPMN modules process will start;
to Petri Net. Section 4 describes a graphical (b) End Event: it indicates where a process
property specification language. Section 5 describes will end.
our verification process of BP and case study.
We develop experiments and analysis in Section 2. Task: is a generic type of work to be done
6. Section 7 concludes the paper, and draws during the course of a BP.
perspectives.
3. Sequence flow: it links two objects in a process
diagram.
2. RELATED WORK
4. Gateways:
Current research in this area are largely concen- (a) And-split Gateway: is where a single
trated on a translation of BPMN models to a formal branch is divided into two or more
language, and the specification of the proprieties parallel branches which are executed
is written in temporal logic, and does not consider concurrently;
a visual language for specifying these proprieties
(b) And-join Gateway: is where two or more
to be verified. In Dijkman et al. (2007), the au-
different branches of the process merge
thors introduce an approach, based on Petri Net,
into one single branch;
to formalize and analyze BPMN while abstracting
data information. However, they only consider safety (c) Or-split Gateway: it routes the sequence
properties of BPMN. In Van der Aalst et al. (2007), flow to exactly one of the outgoing
the authors have developed a tool, called Prom2 , branches based on conditions;
to verify BPMN models. The property specification (d) Or-join Gateway: it awaits one incoming
logic supported by Prom, is restricted to the linear branch to complete before triggering the
temporal logic (LTL). In Sakr et al. (2013), the outgoing flow.
authors have implemented a concept proof of their
approach with existing software namely the open Fig. 1 provides an overview of a subset of BPMN
modeling platform Oryx Decker et al. (2008) and elements related to control-flow specification, these
the BPMN-Q query language Awad (2007). This include sequence flows. An object can be an event,
approach is based on the decomposition of BPMN- activity or gateway. A sequence flow links two objects
Q. However, This verification approach may fail be- in a process diagram and denotes a control flow
cause not all properties of a query can be satisfied relation.
and the decomposition phase is complicated.
To the best of our knowledge, all the above works
assume that the verification phase comes after the
design phase. Thus, a strong background knowledge
of temporal logic is required. Our approach has
the merit of integrating the verification process in
the design stage allowing a gradual validation of
BP. This phase can be avoided by implementing a
specification interface.
3. BASIC DEFINITIONS
Figure 1: The basic elements of BPMN
In this section, we give the basic definitions,
notations of BPMN, and Petri Net used in this paper.
2 http://www.promtools.org/prom6/
2
Visual Specification Language and Automatic Checking of Business Process 95
El Hichami • Al Achhab • Berrada • El Mohajir
3.1.1. Example
For further clarification, we give a simple example
adapted from Raedts et al. (2007) of the recruitment
process. Fig. 2 illustrates the BPMN model of the
hiring process since the creation of the job until the
candidate is rejected or accepted.
Figure 2: BPMN model of the recruitment process Figure 3: Mapping BPMN to Petri Net
3.2. Petri Net 4. A VISUAL LANGUAGE FOR BP PROPERTY
SPECIFICATION (BPVSL)
Petri Net is widely used tool for the representation,
validation and verification of BP Van der Aalst (1997, In this section, we show how the designer can
1998); Barkaoui et al. (2007). A Petri Net is a tuple specify the properties to be verified using a
N = (P, T, F ) where: graphical interface based on the same concepts
as established in BPMN. The framework uses
1. P 6= ∅ is a finite set of places; this specification as a guide to implement the
transformation to LTL MANNA and PNUELI (1992)
2. T 6= ∅ is a finite set of transitions with P ∩T = ∅; or CTL Heljanko (1997) temporal logic, even though
3. F ⊆ (P × T ) ∪ (T × P ) is the flow relation. the designer has no notions of these temporal logic
languages.
A place can contain zero or more tokens. A token
is represented by a black dot. The global state of a Before illustrating the BPVSL that we propose, we
Petri Net, also called a marking, is the distribution give the set of properties that may be needed by the
of tokens over places. Formally, a marking of a Petri designer:
Net N is a function M : P → N. The initial marking
• Safety property: that “nothing bad” will happen,
of N is denoted by M0 .
ever, during the execution of a system like the
An example of Petri Net is shown in Fig. 4.
absence of dead transitions (deadlocks).
3.3. Transforming BPMN models to Petri Net • Liveness property: that “something good” will
happen, eventually, during the execution of a
In order to analyze formally BPMN models, several
system like the absence of cyclical behaviors.
transformations have been proposed Lohmann et al.
(2009); Dijkman et al. (2008). Fig. 3 depicts the • Fairness property: under certain conditions, an
mapping from BPMN tasks, events, and gateways event may occur repeatedly, is a special type of
to Petri Net modules proposed by Dijkman et al. a safety property.
(2008). A task or an intermediate event is mapped
onto a transition with one input place and one output • Invariant property: is a special case of a safety
place. The transition, being labelled with the name of property. This type of property is satisfied with
that task (respectively event), models the execution all system states.
of the task (respectively event). A start or end event
• Response property: if action A occurs then
is mapped onto a similar module except that a silent
eventually action B will occur.
transition is used to signal when the process starts
or ends.
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.
3
Visual Specification Language and Automatic Checking of Business Process 96
El Hichami • Al Achhab • Berrada • El Mohajir
Figure 4: Petri Net model for the recruitment process
• Φ: means Φ is true in next state;
4.1. Response Properties • ♦Φ: means Φ is true in some future state;
To specify the dynamic behavior of a BP, five models • Φ: means Φ is true in all future states;
of response properties (Fig. 5) are considered in our
• Φ1U Φ2: means Φ1 is true in all future states
BP Visual Specification Language (BPVSL).
until Φ2 holds.
4.3. Computation tree logic (CTL)
The syntax of CTL is inductively defined as:
Φ ::= p|¬|Φ|Φ ∧ Φ|Φ ∨ Φ|Φ → Φ.
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;
Figure 5: Patterns of response properties • A♦Φ: means Φ has to hold in some future state
in every execution path;
The following sections provide some of the most
frequently interpretation of this patterns. The • E♦Φ: means Φ has to hold in some future state
designer can use a graphical interface to specify the in some execution path.
source and the target extremities of property to be
verified. Then, the framework proposes the collection For more details see MANNA and PNUELI (1992);
of the gateways and arrow types in order to choose Heljanko (1997).
the desirable semantic.
4.4. Specification language and semantic of Φ1
4.2. Linear temporal logic (LTL)
Temporal logic as extension of boolean logic may be
used as formal language to express the properties
Figure 6: Graphical specification of Φ1
that must be satisfied by the runs of a BPMN model.
LTL is the logic we use in this paper.
Formal semantics of Φ1:
The syntax of LTL is inductively defined as:
• Every time ti is executed, tj has to be executed
Φ ::= p|¬|Φ|Φ ∧ Φ|Φ ∨ Φ|Φ → Φ| Φ|♦Φ|Φ|ΦU Φ.
afterwards: (ti ⇒ ♦tj ), (LTL formula).
Such p is a atomic proposition (task in BPMN). The
intuitive meanings of the associated LTL formulas • All paths from ti to tj : (ti ⇒ A♦tj ), (CTL
are given below: formula).
4
Visual Specification Language and Automatic Checking of Business Process 97
El Hichami • Al Achhab • Berrada • El Mohajir
• Every time ti is executed, tj has to be executed
afterwards: (ti ⇒ ♦tj ), (LTL formula). Formal semantics Φ4:
4.5. Specification language and semantic of Φ2 • 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).
Figure 7: Graphical specification of Φ2 • Every time tasks ti and tj are simultaneously
executed, tk has to be executed afterwards:
((ti ∧ tj ) ⇒ ♦tk ), (LTL formula).
Formal semantics of Φ2:
4.8. Specification language and semantic of Φ5
• 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
Figure 10: Graphical specification of Φ5
on all potential paths: (ti ⇒ (A♦tj ∧ A♦tk )),
(CTL formula).
• Every time ti is executed, tj and tk have to be Formal semantics Φ5:
executed in parallel afterwards: (ti ⇒ (♦tj ∧
♦tk )), (LTL formula). • Every time one of the tasks ti or tj is executed,
it is followed by the task tk : ((ti ∨ tj ) ⇒ ♦tk ),
4.6. Specification language and semantic of Φ3 (LTL formula).
• 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 ),
Figure 8: Graphical specification of Φ3 (LTL formula).
4.9. Safety and Liveness properties
Formal semantics Φ3:
In order to meet the requirements of the designer,
• Every time ti is executed, one of the tasks ti we propose to add for each property to be verified a
or tk has to be executed afterwards: (ti ⇒ sets of properties in order to define safety, liveness,
(♦tj ∨ ♦tk )), (LTL formula). invariant and fairness properties.
• One of the tasks tj or tk eventually is executed 4.9.1. A safety property
after the task ti on each potential path: (ti ⇒ are conditions that are verified along any execution
(A♦tj ∨ A♦tk )), (CTL formula). path. These type of properties are usually associated
• Every time ti is executed, one of the tasks ti with some critical behaviour, thereby they should
or tk has to be executed afterwards: (ti ⇒ always hold. Then, the quantifier () is good for the
(♦tj ∨ ♦tk )), (LTL formula). safety property. For example, in the case of BPMN
model of the recruitment process, the company
4.7. Specification language and semantic of Φ4 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
Figure 9: Graphical specification of Φ4 reach the “good candidate”.
5
Visual Specification Language and Automatic Checking of Business Process 98
El Hichami • Al Achhab • Berrada • El Mohajir
5. VERIFICATION PROCESS AND CASE STUDY types in order to choose between the different
semantics of φ2.
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.
Figure 13: Visual specification 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
Figure 11: Verification process of BPMN 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
As examples, we show how to specify three
gateways and arrow types.
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”.
Figure 14: Visual specification of φ3
6. EXPERIMENTS AND ANALYSIS
In this paper, we use the SPIN tools3 to validate the
LTL formulas. In these experiments, we discuss the
Figure 12: Visual specification of φ1 verification of three models of response properties
Φ1, Φ2 and Φ3 of Section 5.
Example 2: Let φ2 be the property given by: the 6.1. Transforming Petri Net to PROMELA
task “Study CVs” and task “Evaluate interviews”
will be executed in parallel and after task “Receive In order to simulate Petri Net using SPIN, it is
candidate CVs”. This property can be interpreted necessary to translate Petri Net models into SPIN
with the visual presentation of Fig. 13. In fact, models-specified using PROMELA.
the designer has first to select a task “Receive
candidate CVs”, then the designer has to select only In Holzmann (2003), the authors propose a method
the reachable tasks “Study CVs” to be executed to describe a Petri Net into PROMELA that can be
in parallel with the task “Evaluate interviews” as simulated and verified with the SPIN model checker.
the target extremities of φ2. Finally, the framework In this method, a Petri Net system is represented
proposes the collection of the gateways and arrow 3 http://spinroot.com/spin/Man/
6
Visual Specification Language and Automatic Checking of Business Process 99
El Hichami • Al Achhab • Berrada • El Mohajir
as a single process. The process describes each add1(M[19]}
firing of its transitions. An outline of the PROMELA :: atomic{remove1(M[14]) -> fire(X[14]);
program of the Petri Net corresponding to the add1(M[15]}
recruitment process is given bellow: :: atomic{remove1(M[15]) -> fire(X[15]);
add1(M[16]}
#define Place 25 :: atomic{remove1(M[16]) -> fire(X[16]);
#define Transition 25 add1(M[5]}
int M[Place]; /* Marking */ :: atomic{remove1(M[9]) -> fire(X[17]);
int X[Transition]; /* Firing count */ add1(M[17]}
/* A firing of Transition t*/ :: atomic{remove1(M[17]) -> fire(X[18]);
/* remove specifies the change of the add1(M[18]}
marking of preset of t */ :: atomic{remove1(M[14]) -> fire(X[19]);
/* add specifies the change of the marking add1(M[19]}
of postset of t */ :: atomic{remove1(M[19]) -> fire(X[20]);
/* fire (x) increments the element add1(M[20]}
corresponding to t in X[t] */ :: atomic{remove2(M[18],M[20]) ->
#define remove1(x) (x>0) -> x-- fire(X[21]); add1(M[21])}
#define remove2(x,y) (x>0 && y>0) :: atomic{remove1(M[21]) -> fire(X[22]);
-> x--; y-- add1(M[22]}
#define add1(x) x++ :: atomic{remove1(M[22]) -> fire(X[23]);
#define add2(x,y) x++; y++ add1(M[23]}
#define fire(x) x++ :: atomic{remove1(M[23]) -> fire(X[24]);
/* Process representing Petri Net */ add1(M[24]}
init od
{ }
M[0]=1; /* Set the initial marking */
(The PROMELA description of Petri Net shown in Fig. 4)
do
:: atomic{remove1(M[0]) -> fire(X[0]); 6.2. LTL formulas
add1(M[1]}
:: atomic{remove1(M[1]) -> fire(X[1]); The properties to be verified in SPIN have to
add1(M[2]} be expressed as LTL formulas. LTL formulas
:: atomic{remove1(M[2]) -> fire(X[2]); corresponding to to the response properties φ1, φ2
add1(M[3]} and φ3 to be verified can be rewritten as follows:
:: atomic{remove1(M[3]) -> fire(X[3]);
add1(M[4]} • φ1: Does the task “Setup payroll” will happen
:: atomic{remove1(M[4]) -> fire(X[4]); after the tasks “Find candidates” ;
add1(M[5]} LTL formula: [ ]((M [5] >= 1) − > <>
:: atomic{remove1(M[5]) -> fire(X[5]); (M [21] >= 1));
add1(M[6]}
:: atomic{remove1(M[6]) -> fire(X[6]); • φ2: Task “Study CVs” and task “Evaluate
add2(M[7], M[12])} interviews” will be executed in parallel and after
:: atomic{remove1(M[7]) -> fire(X[7]); task “Receive candidate CVs” ;
add1(M[8]} LTL formula: [ ]((M [3] >= 1) − > <>
:: atomic{remove1(M[8]) -> fire(X[8]); (M [12] >= 1 && M [8] >= 1));
add1(M[9]} • φ3: Task “Find candidates” will be executed
:: atomic{remove1(M[8]) -> fire(X[8]); after the tasks “CV not approved” or “Not
add1(M[17]} successful interviews”.
:: atomic{remove1(M[9]) -> fire(X[9]); LTL formula: [ ]((M [15] >= 1 | | M [10] >= 1)
add1(M[10]} − > <> (M [5] >= 1)).
:: atomic{remove1(M[10]) -> fire(X[10]);
add1(M[11]} 6.3. Experimental results
:: atomic{remove1(M[11]) -> fire(X[11]);
add1(M[5]} In this section, we give some statistics in order to
:: atomic{remove1(M[12]) -> fire(X[12]); show the performance of our approach. We present
add1(M[13]} the size, the memory and the verification time of the
:: atomic{remove1(M[13]) -> fire(X[13]); verification of φ1, φ2 and φ3 on the Petri Net related
add1(M[14]} to Fig. 4.
:: atomic{remove1(M[13]) -> fire(X[13]);
7
Visual Specification Language and Automatic Checking of Business Process 100
El Hichami • Al Achhab • Berrada • El Mohajir
We first investigated in Table 1 and Table 2 the REFERENCES
results without Safety properties and with Liveness
properties. ter Hofstede, A., van der Aalst, W., A., Weske,
In Table 3 we present the results with Safety M. (2003) Business process management: A
properties(invalid deadlock) and without Liveness survey. In Weske, M., ed.: Business Process
properties. Management. Volume 2678 of Lecture Notes in
Computer Science. Springer Berlin / Heidelberg.
Table 1: Experiments without Safety properties and with
Liveness properties(acceptance cycles) Mohammed AbuJarour and Ahmed Awad. (2014)
Web Services and Business Processes: A Round
Trip. Web Services Foundations : pp. 3-29.
States Transitions Memory Times
(Mb) (s) OMG. (2011) Business Process Modeling Notation
φ1 8310907 1.4110983e+08 1023.946 83.8 (BPMN) Version 2.0. OMG Final Adopted Specifi-
φ2 8311225 1.2663418e+08 1023.946 74 cation. Object Management Group.
φ3 8311136 1.2658587e+08 1023.946 71.5
T. Takemura. (2008) Formal semantics and verifica-
tion of BPMN transaction and compensation. In
Table 2: Experiments without Safety properties and Proc. of APSCC 2008, pp. 284-290. IEEE.
with Liveness properties(acceptance cycles and enforce
fairness property) J. W. Bryans, J. S. Fitzgerald, A. Romanovsky, and
A. Roth. (2009) Formal modelling and analysis
States Transitions Memory Times of business information applications with fault
(Mb) (s) tolerant middleware. In Proc. of ICECCS 2009, pp.
φ1 8059677 1.3712059e+08 1023.946 83.5 68-77. IEEE Computer Society.
φ2 8059995 1.2277647e+08 1023.946 71.4
O. El Hichami, M. Al Achhab, I. Berrada and B.
φ3 8047291 1.2276921e+08 1023.946 70.1
El Mohajir. Graphical specification and automatic
verification of business process, the International
Table 3: Experiments with Safety properties(invalid Conference on Networked systems. NETYS 2014,
deadlock) LNCS 8593, Springer, pp. 1-6.
W.M.P. van der Aalst and B.F. van Dongen. (2013)
States Transitions Memory Times
Discovering Petri Nets From Event Logs. T. Petri
(Mb) (s)
Nets and Other Models of Concurrency 7: 372-
φ1 8059582 64672621 1023.946 27.2 422.
φ2 8059582 57992022 1023.946 24.1
φ3 8004931 55834127 1023.946 25.6 Dirk Fahland, Cdric Favre, Jana Koehler, Niels
Lohmann, Hagen Volzer, Karsten Wolf. (2011)
Analysis on demand: Instantaneous soundness
checking of industrial business process models.
7. CONCLUSION
Data Knowl. Eng. 70(5): pp.448-466.
The paper proposes a visual language for specifying T. Murata and J.Y. Koh (1989) Petri nets: Properties,
business process behavior. We use BPMN to Analysis and Applications. an invited surve y
modelize BP, Petri Net as underlying formal paper, Proceedings of the IEEE, Vol.77, No.4
foundations, and spin model checker to perform pp.541-580.
automated analysis. The principal objective of this
paper is to propose a graphical framework which use O. El Hichami, M. Al Achhab, I. Berrada, R. Oucheikh
the same notation as established in BPMN. In this and B. El Mohajir. (2014) An Approach Of
way the designer can specify and validate the BP Optimisation And Formal Verification Of Workflow
properties during the design phase. Several formal Petri Nets. Journal of Theoretical and Applied
semantics for these properties are expressed as Information Technology, Vol.61, No.3 pp. 486-495.
temporal logic formulas.
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.
8
Visual Specification Language and Automatic Checking of Business Process 101
El Hichami • Al Achhab • Berrada • El Mohajir
R. M. Dijkman, M. Dumas, and C Ouyang. (2007) Heljanko, K. (1997) Model checking the branching
Formal semantics and analysis of BPMN process time temporal logic CTL, Research Report A45,
models using Petri nets. Technical Report 7115, Helsinki University of Technology, Digital Systems
Queensland University of Technology, Brisbane. Laboratory, Espoo, Finland.
W.M.P. van der Aalst, B.F. van Dongen, C.W. G nther, G.J. Holzmann. (2005) The Model Checker Spin,
R.S. Mans, A.K. Alves de Medeiros, A. Rozinat, Addison-Wesley, p.596, 2003.
V. Rubin, M. Song, H.M.W. Verbeek, and A.J.M.M.
Weijters. (2007) ProM 4.0: Comprehensive Sup-
port for Real Process Analysis. In J. Kleijn and A.
Yakovlev, editors, Application and Theory of Petri
Net and Other Models of Concurrency (ICATPN
2007), volume 4546 of LNCS, Springer-Verlag,
Berlin, pp. 484-494.
Sherif Sakr, Ahmed Awad, Matthias Kunze. (2013)
Querying Process Models Repositories by Aggre-
gated Graph Search, in Springer Berlin Heidel-
berg. Volume 132, pp 573-585.
Decker, G., Overdick, H., Weske, M. (2008) Oryx
- Sharing Conceptual Models on the Web. In:
Conceptual Modeling - ER. LNCS 5231, Springer
Verlag, pp. 536-537.
Awad, A. (2007) BPMN-Q: A Language to Query
Business Processes. In EMISA, pp. 115-128.
Ivo Raedts, Marija Petkovic, Yaroslav S. Usenko, Jan
Martijn E. M. van der Werf, Jan Friso Groote,
and Lou J. Somers. (2007) Transformation of
BPMN Models for Behaviour Analysis. MSVVEIS,
INSTICC PRESS, pp. 126-137.
W.M.P. van der Aalst. (1997) Verification of Workflow
Nets. ICATPN 97, Volume 1248 of LNCS, pp. 407-
426.
W.M.P. van der Aalst. (1998) The Application of
Petri Net to Workflow Management. The Journal
of Circuits, Systems and Computers, Vol.8, No.1,
pp. 21-66.
Kamel Barkaoui and Rahma Ben Ayed and Zohra
Sba. (2007) Workflow Soundness Verification
based on Structure Theory of Petri Net, IJCIS
Journal, 51-62.
Niels Lohmann, Eric Verbeek, Remco M. Dijkman.
(2009) Petri Net Transformations for Business
Processes - A Survey. T. Petri Net and Other
Models of Concurrency 2. 46-63, Springer Berlin
Heidelberg.
Dijkman, Remco M., Dumas, Marlon, Ouyang,
Chun. (2008) Semantics and analysis of business
process models in BPMN. Information and
Software Technology, 50(12), pp. 1281-1294.
Z.MANNA, A.PNUELI. (1992) The temporal logic of
reactive and concurrent systems, Springer-Verlag
New York, Inc., New York, NY, USA.
9