Because of their expressive power, Petri nets are widely used in the context of concurrent and distributed systems. We study in this paper a sub class of time Petri nets, named time open workflow nets (ToWF-nets), used to interconnect time constrained business processes. To interact correctly with each other, these processes have to be compatible. This include not only composability of the involved processes but also the correct execution of the overall composite system. In this context, we suggest in this paper to study the compatibility of ToWF-nets in different aspects and to provide a formal approach to characterize and verify this property. This approach is based on qualitative and quantitative analysis ensured by TCTL model checking.
The workflow technology has shown a great interest to be adopted within
organizations or even inter organizations. A workflow is the result of the automation
of a business process, in whole or in part [
Open workflow nets (oWF-nets) form a sub class of Petri nets which is
successfully used to model workflow processes which communicate with other
partners via interfaces. This class is promisingly used in the context of Web services
orchestration and choreography. In fact each service in a composition is
modeled by a workflow net augmented by interface places used to communicate with
other services. In this way, one can guarantee the conversation between the
processes interacting with each other. The conversation considered here is involved
through the two well known behaviors: operational and control. An operational
behavior is a behavior specific to each partner according to its business logic. A
control behavior describes the general behavior of any process related to
composite Web services. While we focused in a previous work [
Several time Petri nets extensions were proposed in the literature which
differ in their semantics and their analysis techniques. We propose to adopt in this
work the time Petri nets, proposed by Merlin [
Dealing with time in inter organizational processes, we propose to study the compatibility of the processes communicating together. This property is not only related to the ability of processes to communicate (i.e. composability) but also to the correct and deadlock-free execution of the composite process. In this context, we propose to define compatibility classes of ToWF-nets and to emphasize a method of their verification.
To verify ToWF-nets compatibility, we propose to use formal methods due to their solid theoretical basis. More precisely, we present an analysis method based on model checking of the studied properties. In fact, Model checking is an automated verification technique for proving that a model satisfies a set of properties specified in temporal logic. Given a concurrent system ⌃ and a temporal logic formula ', the model checking problem is to decide whether ⌃ satisfies '. Hence, we have to formulate in temporal logic the properties to be verified. This kind of verification is situated at the design phase, allowing thus to find design bugs as early as possible and therefore to reduce the cost of failures. This, especially, permits us to check as early as possible if two or more processes are compatible before their composition. We express the proposed compatibility properties in Timed Computation Tree Logic (TCTL).
The rest of this paper is organized as follows. We propose in section 2 the ToWF-nets to model inter organizational workflow processes with timing delays. The same section presents the semantics of ToWF-nets in terms of states and their evolution and exposes a case study. Section 3 is dedicated to present some results of the reachability analysis of ToWF-nets. We focus in section 4 on the verification of ToWF-nets compatibility. We begin with expressing the properties in TCTL and then we present some experiments in Romeo model checker. Section 5 exhibits related work and finally section 6 concludes the paper and announces future work. 2
In this section, we propose a new sub class of time Petri nets modeling workflow processes with interface places used to communicate with other partners. To begin with, we present a Petri nets modeling of communicating processes and then we propose a time extension. 2.1
Nowadays, many organizations are implementing their business functionality and outsource their services on the internet. Thus, the selection as well as inter organizational and heterogeneous integration with efficiency and effectiveness of Web services during the execution has become an important step in Web services applications. In particular, if no service can meet the needs of the user, there should be a possibility to combine existing services to meet the demands required by the user. This trend has led to the notion of the composition of Web services.
In fact, the composition or aggregation of Web services is a process that involves building new services or aggregates called composite services by assembling existing services. The composite service is a value added service that can be the distribution of basic services or composite ones.
This composition can be modeled by means of a Petri net class named open
workflow nets [
As mentioned above, open workflow nets are mainly an extension of workflow
nets (WF-nets) to model workflow processes which interact with other workflow
processes via interface places. Simple WF-nets [
A Petri net is a 4-tuple N = (P, T, F, W ) where P and T are two finite
nonempty sets of places and transitions respectively, P \ T = ; , F ✓ (P ⇥ T )[ (T ⇥ P )
is the flow relation, and W : (P ⇥ T ) [ (T ⇥ P ) ! N is the weight function of N
satisfying W (x, y) = 0 , (x, y) 2/ F . If W (u) = 1 8 u 2 F then N is said to be
ordinary net and it is denoted by N = (P, T, F ). For every node x 2 P [ T , the
set of input nodes of x is defined by •x = {y|(y, x) 2 F } and the set of output
nodes is denoted by x• = {y|(x, y) 2 F }. We refer the reader to [
A Petri net which models a workflow process is said to be a WF-net [
For a composition, we propose to model each Web service by a WF-net specifying the set of tasks to be performed and their routing. The conversation between the different Web services is ensured by communication places used for messages sending. We are thus using open WF-nets (oWF-nets) which generalizes the classical WF-nets by introducing interface places for asynchronous communications with partners. Hence, we model a composition by a set of oWFnets communicating via interface places. These places connect only transitions of different processes. 2.2
When incorporating time constraints, different extensions of Petri nets were proposed. In general, when the time constraints are specified by constants(durations), the associated extension is said Timed Petri nets. This consider constant durations attached to places (P-Timed Petri nets) or transitions (T-Timed Petri nets). When these constraints are specified by intervals (delays) specifying the minimum and the maximum amounts of time needed for transitions’ firing, the associated extension is called Time Petri nets. These intervals are attached to places (P-Time Petri nets), transitions (T-Time Petri nets) or arcs (A-Time Petri nets) leading thus to different extensions with variant semantics.
Petri nets form a powerful formalism for the expression of control flow in
business processes [
In [
Since this time consideration is flexible and given that we are interested by modeling the composition of workflow processes with time constraints, we propose the time open workflow net model (ToWF-net). This model associates a static time interval to each transition of an open workflow net to express the execution time or delay of corresponding activity. The formal definition of a ToWF-net model net is the following:
A Time Open Workflow Net N is a tuple (P, T, F, F I, I, O) with: • P is a set of places, • T is a set of transitions, • I is a set of places representing input interfaces which are responsible for receiving messages from other services: •I = ; . • O is a set of places representing output interfaces that are responsible for sending messages to other services: O• = ; . • I, O and P are disjoint. I and O connect transitions of different partners. • F ✓ ((P [ I) ⇥ T ) [ (T ⇥ (P [ O)) is the flow relation, • F I : T ! Q+ ⇥ Q+ [ {1} is the function that associates with each transition t 2 T a static firing interval, i.e. F I(t) = [minF I(t), maxF I(t)] where minF I(t) and maxF I(t) are rational numbers representing respectively the minimal and maximal firing time,
The marking of N is a vector of NP such that for each place p 2 P , M (p) is the number of tokens in p. The initial marking of N is Mi knowing that Mp is used to denote a marking for which M (p) = 1 and M (q) = 0 8 q 2 (P [ I [ O)\{p}.
A transition t is said to be enabled in a marking M if the required tokens are present in the input places of t. We denote by En(M ) the set of all the transitions enabled in the marking M . A transition t is said disabled by the firing of t0 in M if it is enabled in M but it isn’t in M • t0. When focusing of newly enabled transitions after firing a transition t from M and leading to M 0, we denote by N En(M, t) the set of transitions enabled after this firing.
N En(M, t) = {t0 2 En(M 0)|t0 = t _ ¬ M • t +• t0}.
When a transition t becomes enabled, its firing interval is set to its static firing interval F I(t). The lower and upper bounds of F I(t) decrease synchronously with time, until t is fired or disabled by another firing. t can fire, if the lower bound of its firing interval reaches 0, but when upper bound of its firing interval reaches 0, t must be fired without any additional delay (strong semantic). The firing takes no time but may lead to another marking.
Let us define first the state of a ToWF-net and then the transition relation. Definition 2 A state in a ToWF-net represents the state of the process modeled with ToWF-net after the occurrence of an event. Formally, a state in a ToWFnet is a pair (M, Int) where: – M is a marking, – Int is a firing interval function, Int : En(M ) ! Q+ ⇥ Q+ [ {1} . We denote Int(t) = [minInt(t), maxInt(t)].
The initial state of a ToWF-net is (M0, Int0) where M0 = Mi (since in a ToWF-net, only i contains initially one token) and Int0(t) = F I(t) 8 t 2 En(M0)
Starting from the initial state (M0, Int0), the net evolves following the occurrence of events. An event corresponds to either a transition firing or a time progression. Hence, the transition relation between a state s1 = (M1, Int1) and s2 = (M2, Int2) is defined by !t in case of a firing and by !d in case of time progression. The conditions and the computation of the resulting state after an event occurrence are defined as follows: 1. s1 !t s2 if and only if s2 is immediately reachable from s1 by firing the transition t, i.e. t 2 En(M1) and minInt1(t) = 0, M2 = M1 • t + t•, and 8 t0 2 En(M2), Int2(t0) = ⇢ F I(t0) if t0 2 N En(M1, t)
Int1(t0) otherwise 2. s1 !d s2 8 d 2 R if and only if the state s2 is reachable from s1 by time progression with d time units, i.e. minInt1(t) + d maxF I(t), M2 = M1, and 8 t 2 En(M1), Int2(t) = [M ax(0, minInt1(t) d), maxInt1(t) d] Therefore, the semantics of a ToWF-net N is defined by a transition system (S, s0, ! ) where S is the set of all the states reachable from the initial state s0 by the transition relation ! defined above. 2.3
In order to illustrate the proposed ToWF-net, we propose to study the process of awarding of pensions to handicapped persons. This process requires the collaboration of three organizations: • The prefecture which manages scholarships and grant of license to the disabled. • A medical entity that is responsible for negotiating the date of appointments with patients and collecting the medical informations. • The Town Hall which establishes certificates, births extracts, etc.
The allocation of pension process is seen as a collaboration between the services offered by these organizations.
In fact, citizens with disabilities ask a government scholarship. To start the process, citizens request the form corresponding to the prefecture. Once the citizen receives the form, he fills it and sends it to the prefecture. The latter seeks medical entity to consider disability that the citizen presents. Medical entity subsequently contacts the citizen to negotiate with him about a date of appointment. Once an appointment is fixed, and after reviewing the citizen, the entity establishes a medical examination report and forwards it to the prefecture. Meanwhile, the prefecture asked the town hall to establish a certificate of residence of the citizen. Once the certificate of residence and the medical report is received, the prefecture makes the final decision.
The figure 1 shows a screenshot of this composition involving the four processes relevant to the Applicant, the Prefecture, the Town Hall and the Medical Unit.
These processes are interconnected with available interfaces that facilitate communication and exchange of messages between them. These interfaces correspond to places denoted by Isn (for input interfaces) and Osn (for output ones), where s is the service number and n is the interface number in each category. Note that each input interface place of a service has an equivalent output interface of another service and this will guarantee the services communication. For sake of clarity, in this example, the interfaces are given names which explain the sequence of exchanged messages between partners.
The various services are forced to respect the different temporal properties of each service, in what follows , we mention a few of them: • Once the medical entity proposes dates for appointment to the citizen, it must receive the confirmation within 24 hours. • Once the application for the grant is received, the prefecture sends its final decision to the citizen, after at least 49 hours and not more than 180 hours. • The medical report may be sent to the prefecture after at least 24 hours and up to 48 hours of sending the medical examination. • The receipt of the result of the request is within 210 hours after sending the request of the purse. • Two hours is the maximum time to review a citizen in medical entity. • The time of receipt of the certificate of residence and review of citizen ratio is up to three hours. • Negotiation of the appointment date between the citizen and the medical entity runs for up to one hour.
We present in the following section the analysis of reachability of the Web
services composition modeled by ToWF-nets and we expose the case study
reachability analysis in the tool Romeo [
After the formal definition of ToWF-nets, we focus now on their reachability analysis. This analysis is based on the efficient construction of the state space.
By analogy with the marking graph defined in the context of an ordinary Petri net, we define a state space by a graph containing all accessible states of a ToWF-net from the initial state. Therefore, to calculate the state space of a ToWF-net, we must be able to calculate the reachable states by activating the enabled transitions.
Definition 3 The state space of a ToWF-net has the following structure: SS = (S, ! , s0); where S is the set of nodes in form (M, Int) representing the reachable states from the initial one s0 = (Mi, Int0) ; ! represents the transition relation which defines the evolution from one state to another.
S = {s|s0 !⇤ s} is the set of reachable states of the model, and !⇤ is the reflexive and transitive closure of ! .
( vi
vj bij i, j 2 [0..n], bij 2 Q
The reachability analysis [
In return, the state class method is intended to provide a finite representation of the infinite state space of any bounded time Petri net.
Technical classes produce for a large class of time nets a finite representation of their behavior states, which allows a reachability analysis similar to that permitted for Petri nets by the technique of marking graph.
The state classes can be represented by a marking and a firing domain. Formally, a state class is a couple (M, D) where M is a marking and D is characterized by a set of atomic constraints over the firing delays of enabled transitions: minF I(t) t maxF I(t) 8 t 2 En(M ).
Note that the initial class coincides with the initial state of the network. This initial class is (M0, D0) where M0 = Mi and D0 corresponds to the firing domains of transitions enabled in M0.
All states within the same node share the same untimed information and the
union of their time domains is represented by a set of atomic constraints handled
efficiently by means of a Difference Bound Matrix (DBM) [
v0 = 0
In terms of behavior, this state classes group preserves highly the states traces, and thus the safety properties.
The computation of the state class graph is necessary at this point to
perform the various reachability analysis. Among the abstractions proposed in the
literature [
Romeo [
Therefore, we used Romeo to generate the SCG of our case study. We begun with composing the different services by superposing the interface places which correspond to the same interface communication. We then simulated the overall obtained net in Romeo. Figure 2 presents a snapshot of the case study analysis conducted in Romeo and especially the beginning of the file generated by Romeo and which contains the SCG.
The analysis of the state space is very significant to the extent that it can reveal important characteristics of the modeled system, about its structure and dynamic behavior. However, for a more accurate verification, we should not be limited to this type of checking rather another specific properties. Indeed, we focus in this section on the formal verification of compatibility properties of ToWF-nets. We propose to use model checking method to verify these properties since this method permits an exhaustive verification over all the possible executions. Given a concurrent system ⌃ and a temporal logic formula ', the model checking problem is to decide whether ⌃ satisfies '. Hence, we have to formulate in temporal logic the properties to be verified.
Real systems often have behaviors that depend on time. The ability to manipulate and model the temporal dimension of the events that take place in the real world is fundamental in many applications. These applications may involve banking, medical, or multimedia applications. The variety of applications motivate many recent studies that aim to integrate all the features necessary to take into account the time during verification.
TCTL (Timed Computational Tree Logic) is a timed extension of the temporal logic CTL. TCTL added to CTL a quantitative information on the delays between actions. It is built from atomic propositions, logical connectors and temporal operators (U, F, G, X, etc.). The TCTL temporal logic can be used to check the properties of a time Petri net.
The syntax of TCTL formulas is inductively defined by: ' ::= false | ¬' | ' ^ ' | A(' UI ')| E(' UI ') where p denotes a proposition, ' denotes a formula and I = [a, b] or [a, 1[ with a 2 N and b 2 N.
A and E are temporal quantifiers over the set of executions. A' announces that all the executions from the current state satisfy the property '. E' states that from the current state, there exists an execution which satisfies '. Finally ' UI means that the property ' is true until is true, and will be true in the time interval I.
We can use other compositional temporal operators [
Semantically, TCTL formulas are interpreted on states and execution paths of
a model M = (S, V ) where S is a transition system and V is a valuation function
that associates with each state the set of atomic propositions it satisfies. [
To interpret a TCTL formula on an execution path, we introduce the notion of dense execution path. Let s 2 S be a state of S, ⇡ (s) the set of all execution paths starting from s, and ⇢ = s0 ! d1t1 s2... an execution path of s. The d0t0 s1 ! dense path of the execution path ⇢ is the mapping ⇢ ˆ : R+ ! S defined by: ⇢ ˆ(r) = si + such that r = Pij=10 dj + , i 0 and 0 di.
The formal semantics of TCTL is given by the satisfaction relation defined as follows: – M , s 2 f alse, – M , s ✏ iff 2 V (s), – M , s ✏ ¬' iff M , s 2 ', – M , s ✏ ' ^ iff M , s ✏ ' and M , s ✏ , – M , s ✏ 8 (' [ I ) iff 8 ⇢ 2 ⇡ (s) 9 r 2 I, M , ⇢ ˆ(r) ✏
8 0 r0 r M , ⇢ ˆ(r0) ✏ ', – M , s ✏ 9 (' [ I ) iff 9 ⇢ 2 ⇡ (s) 9 r 2 I, M , ⇢ ˆ(r) ✏ 8 0 r0 r M , ⇢ ˆ(r0) ✏ ', and and
The Time Petri net model is said to satisfy a TCTL formula ' iff M, s0 ✏ '.
The logic TCTL allows writing temporal properties with a quantification of
the time. We chose this approach because it is decidable and PSPACE-complete
for bounded Petri nets [
The authors of [
Definition 4 The temporal logic TPN-TCTL is defined inductively by: TPN-TCTL ::= false | ' | ¬' | ' _ | ' ^ | ' ) | E'UI | A'UI | EGI ' | AGI ' | AFI ' | EFI ' | AG( 1 ) AF[0,d] 2).
I = [a, b] or [a, b[ with a 2 N and b 2 N [ {1} .
1 and 2 are propositions on markings.
8 G( 1 ) 8 F[0,d] 2) means that from the current state, any occurrence of marking 1 is followed by an occurrence of marking 2 less of d units of time later.
Romeo permits a practical implementation of the verification of properties described in TPN-TCTL. It is therefore possible to model check on the fly temporal quantitative properties. That’s why we investigate in the following section the TCTL expression of the compatibility property and hence its verification in Romeo.
Before this, let us recall the notation used by Romeo to implement a TPNTCTL property:
TPN-TCTLRomeo = E(p)U [a, b](q) | A(p)U [a, b](q) | EF [a, b](p) | AF [a, b](p) | EG[a, b](p) | AG[a, b](p) | EF [a, b](p) | (p) ! [0, b](q).
where p, q: GMEC; U : until; E: exists; A: forall; F : eventually; G: always; ! : response; a: integer; b integer or inf (to denote 1).
GM EC = a⇤ M (i){+, } b⇤ M (j){<, <=, >, >=, =}k | deadlock | bounded(k) | p and q | p or q | p ) q | not p.
M : keyword (marking); deadlock, bounded: keywords; i, j:place indexes; a, b, k :integers ; ⇤ , +, , and, or, ) , not: usual operators ; p, q: GMEC
The syntax (p) ! [0, b](q) denotes a leads to property meaning AG((p) imply AE[0, b](q)). E.g. (p) ! [0, b](q) holds if and only if whenever p holds eventually q will hold as well in [0, b] time units. 4.2
From a behavioral point of view, two (or more) processes are said to be compatible if they can interact correctly: this means that they can exchange the same type of messages and the composite system does not suffer from the deadlock problem. This leads us to distinguish between a syntactic compatibility which concerns the verification of the interfaces conformance and a semantic compatibility which is related to check the absence of deadlocks. We investigate in this paper the analysis of the semantic compatibility.
But before this, let us define the composite system obtained from the superposition of a number of syntactically compatible ToWF-nets. The composed system N of nbX ToWF-nets N1... NnbX consists of all ToWF-nets which share interface places, i.e. every place of N which is an input interface of a WF-net is also an output place of another WF-net in the composition. Trivially, N can be seen as a time Petri net with nbX input places and nbX output places. The initial marking of N is M0 = Psn=bX1 is.
According to [
In this direction, we define three classes of compatibility: • Partial compatibility: A composed system N is partially compatible if it is deadlock-free. • Total Compatibility: A composed system N is compatible if N is already partially compatible and furthermore, it guarantees the proper termination. • Perfect compatibility: A composed system is perfectly compatible if it verifies the total compatibility as well as the deadline constraints.
We focus here on formulating the three types of compatibility properties: partial compatibility, total compatibility and perfect compatibility. Let us consider the following: • nbX: is the number of processes; • nbp: is the number of places in a given process; • nbi: is the number of interface places available in a composition; • is: is the input place of the process number s. • fs: is the output place of the process number s. – Partial compatibility
To assure its partial compatibility, we have to check the absence of deadlock in a composition. The process is deadlock-free if there is a transition allowed for any marking except the final marking Mfin in which all the final places fs (s = 1..nbX) are marked. This property is expressed as follows:
8 M 2 [M0i, Mfin 2 [M i
In TCTL, the deadlock-freeness can be expressed as "for all the executions from the initial state, no deadlock will be encountered until the final state is reached". For the final state, it suffices to check if the final places are marked. Hence, the expression of the partial compatibility in TCTL is given as follows: AG[0,1 [((not M F ) ) not deadlock) where deadlock is a proposition which returns true iff there is no enabled transition from the current state; and M F is a proposition on the marking Mfin in which each final place contains at least one token.
nbX
M F = s^=1M (fs) >= 1
Here we focus only on the arrival of tokens to final places and we don’t care if the other places contains tokens or not.
– Total compatibility
Having expressed the partial compatibility, we focus here on the expression of the property of proper termination in TCTL. This property allows the process to complete its execution in any case, but at the time of termination, all places of ToWF-nets must be empty except for the final places which must have one token. Verifying the proper termination consists in checking the existence of a marking M for which all places are empty except the output ones. The expression of this property is given as follows: 8 M 2 [M0i : M (fs) 1 8 s 2 { 1, .., nbX} )
M = Psn=bX1 fs In TCTL, this property (proper termination) is formulated as follows:
AF[0,1 [ StrictM F
Where StrictM F is a proposition on the marking ensuring exactly one token in each final place fs and no tokens in all the other places including the interface places.
nbX nbip StrictM F = s^=1 (p^=1(M (p) = 0) ^ (M (fs) = 1)) ^ nbi (i=^1M (Ii) = 0)
In this definition, we used nbip to denote the number of places except the final place for a process.
– Perfect compatibility
Here, we have to check the deadlock-freeness and the proper termination taking into account the overall deadline constraint.
Let us consider that a process has to reach his final state in T m time units. The proper termination within this delay is expressed as follows:
AF[0,T m] StrictM F
Hence, the perfect compatibility of a composition of ToWF-nets is ensured iff: – AG[0,T m]((not M F ) ) – AF[0,T m] StrictM F
We report in this section some results related to the verification of compatibility and soundness properties of the composition of ToWF-nets. This verification is ensured by Romeo since it implements an on the fly model checking algorithm of TPN-TCTL properties.
Let us study the simple composition of ToWF-nets of figure 3. One can easily see that no deadlock will be encountered until the final places will be marked. Hence the partial compatibility is satisfied as proven in figure 4. Nevertheless, the execution of transitions T4 and T5 of the second process leads to two tokens in the place f2; which leads to violate the property of total compatibility. Figure 5 shows the negative result for this property and draws a trace.
Let us now return to the case study given in figure 1. In order to check the partial compatibility of the involved processes, we formulate the correspondant TCTL formula as follows :
AG[0, inf ]((not (M (30) >= 1 and M (21) >= 1 and M (23) >= 1 and
M (28) >= 1)) ) not deadlock)
Where 30, 21, 23 and 28 are the indexes associated by Romeo to respectively the places f1, f4, f3 and f2.
Figure 6 draws a snapshot of a the verification of the partial compatibility of the four processes involved in the composition. As we can see in the figure, the result is true and hence the partial compatibility is ensured. The total compatibility characterized by the partial compatibility and the following formula is also verified for this example:
AF [0, inf ](M (30) = 1 and M (21) = 1 and M (23) = 1 and M (28) = 1 and M (1) = 0 and M (1) = 0 and M (2) = 0 and M (3) = 0 and .. and M (36) = 0)
The perfect compatibility ensuring a proper termination with deadlock
freeness within 210 hours is also verified for the example. However if we suggest a
perfect compatibility in less than 210 hours, the result is "false".
Several works dealt with compatibility analysis of Web services modeled either
by open workflow nets or other formalisms. Wil M. P. van der Aalst and al.
[
Lucas Bordeaux and al. [
Marlon Dumas and al. [
Wei Tan and al. [
These works dealt with non timed processes while we focus on those
augmented by time information. Focusing on time constraints, Nawal Guermouche
and al. [
Open workflow nets form a sub class of Petri nets which has been widely and successfully used to model inter organizational business processes. In particular, they successfully form a solid theoretical basis for modeling and analysis of Web services composition. From a software engineering point of view, the construction of new services by composing existing ones raises a number of challenges. The most important is the challenge to guarantee a correct interaction of independent, communicating pieces of software. In deed, due to the message sending nature of service interaction, many delicate errors might take place when several services are put together (unreceived messages, deadlocks, contradictory behaviors, etc.). So far, it is necessary to ensure the proper functioning of each service involved in the composition as well as their ability to be composed, their good communication and the validity of their messages exchange.
In this context, we investigated in this paper the verification of open workflow nets compatibility as a main feature to ensure a correct composition and to prevent eventual errors from occurring. In addition, we extended the oWF-nets by timing constraints specifying the activities delays. For the proposed model baptised Time oWF-net, we studied its semantics in terms of states evolution. Then, we defined compatibility classes relative to ToWF-nets and emphasized a formal method of their verification based on TCTL model checking. We finally studied a case study in which four services interact with each other to reach a common goal which is the awarding of pensions of handicapped persons. We conducted a reachability analysis of this example in conformance with the method we propose and we model checked some of the proposed properties with the time Petri net analyser Romeo. We presented, in addition, a simple example with a violated property in order to show the generation of a counter example.
As a perspective, we propose to study the parametric verification of ToWFnets. In deed, this supposes to treat ToWF-nets modeling concurrent instances and thus the consistency of time properties is of great interest.