Collaborative systems design is today a complex process especially where constraints such as tasks delays or resources handling have to be considered. In addition to a well constructed model of a workflow system, a prior and rigorous verification phase is important to ensure a correct execution of the system. In this direction, we are interested in this paper by the modeling and the analysis of interacting processes in particular those constrained by timing delays. First, we present the Time open Workflow nets (ToWF-nets) which stand for a sub-class of Petri nets dedicated to model any business process which interact with other partners via interface places in order to meet a common goal. Then, after recalling the semantics of ToWFnets, we investigate in presenting our recent results in quantitative verification of properties related to the correct communication of various ToWF-nets. We show how to make a TCTL based model checking of the studied properties. Finally, we extend our analysis approach of ToWF-nets to cover concurrent processes leading thus to propose a parametric verification of ToWF-nets.
Nowadays, collaboration in organizations is more and more sought since it allows to end users to benefit from more enhanced and complex services. Although it is possible to allow complex services with a single organization, it is almost impossible to provide, in this case, simple services nor to reuse them. So, it is important to provide simple services and to allow their composition, if necessary, for more complex tasks. For instance, manufacturing systems can be seen as a network of servers and queues. This system process can be seen as a composition of multiple services interacting together to fulfill a unique goal. As an example, we mention a factory which make shirts. The first stage in shirt manufacturing is the cutting of the material to different shapes. Then, the next stage is to sew the pieces together. Finally buttons and a quick iron are added. This composition is more and more studied when treating inter organizational processes. We mention for example a manufacturing enterprize which has to communicate with clients, suppliers, etc. in order to fulfill the manufacturing task. Thus the notion of services composition is of great need and that’s why it is very studied in academic as well as industrial environment.
In collaborative systems in general, different partners, having their own processes, interact together in order to achieve a common goal. We focus in this paper on the modeling and the analysis of such systems involving multiple communicating processes. In the modeling phase, we propose to use Time Open Workflow Nets (ToWF-nets), a sub class of Time Petri Nets (TPN) to model workflow processes with timing delays and with ability to communicate with partners. A ToWF-net consists of an open workflow net (oWF-net) in which we associate with each transition a minimum and a maximum amount of time needed to its execution. An oWF-net is a workflow net augmented with special places called interface places and used to interact with other processes. For the purpose of analysis, we propose to enhance a formal verification due to solid theoretical basis of formal methods. More precisely, we adopt an analysis method based on the well known model checking techniques. 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 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 properties in Timed Computation Tree Logic (TCTL). The rest of the paper is organized as follows. Section 2 is dedicated to the presentation of ToWFnets for modeling interacting processes which are constrained by timing delays. In this section, we present the semantics of the model in terms of states and the states evolution. In section 3, we highlight quantitative analysis results of ToWF-nets. We recall first the principle of TPN-TCTL temporal logic, then we characterize some properties of interest and express them in this temporal logic and finally, we detail how to model check these properties via several examples. We focus in section 4 on a parametric verification of ToWF-nets composition and on some experiments in Romeo model checker. Finally, section 5 presents related work and section 6 concludes the paper with a discussion and a proposition of future work.
This section is dedicated to present Time open Workflow nets (ToWF-nets) : a Petri nets sub class allowing to model workflow processes communicating with partners via interface places. After defining ToWF-nets model and semantics, we expose some results on reachability analysis.
To model a composition of interacting processes,
we refer to Petri nets due to their expressive
power as well as their theoretical basis. The well
known Petri net class used in this modeling is
named open workflow nets (oWF-nets) (
As mentioned above, oWF-nets nets are mainly
the extension of workflow nets (WF-nets) to
model workflow processes which interact with other
processes via interface places. Simple WF-nets
(Sbaï and Barkaoui (2013, 2012)) is a result of
Petri nets’ application to workflow management. The
choice of Petri nets is explained by the fact that they
form a powerful formalism expressing the control
flow in business processes (
Commonly, a Petri net is a 4-tuple N = (P; T; F; W )
where P and T are two finite non-empty 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 8u 2 F then N is called an 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 = fyj(y; x) 2 F g and the output nodes of x form
a set denoted by x = fyj(x; y) 2 F g. We refer the
reader to (
A Petri net which models a workflow process is called
a WF-net (
For processes composition, we propose to model
each process by a WF-net describing the tasks
to be performed as well as their routing. Then,
the conversation between the involved processes
is ensured by the communication places used for
the conversation and/or the messages sending.
Thus, we are using open WF-nets (oWF-nets) which
extend the classical WF-nets by integrating interface
places to ensure asynchronous communication with
the different partners. Hence, a composition is
modeled by a set of oWF-nets interacting via
interface places. Note that these places are used to
connect only transitions from different processes.
Now when we focus on incorporating time
constraints, we find different proposals which are based
on extensions of Petri nets. In general, the time
constraints are modeled either by durations or delays.
When they are specified by durations (constants),
the extension associated is said to be Timed Petri
nets. These constant durations are either attached
to places (the subclass is known as P-Timed Petri
nets) or to transitions (T-Timed Petri nets). In case
of delays adoption, the constraints are specified by
means of intervals specifying the minimum and the
maximum amounts of time representing the
transitions firing delays, 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.
In the case of workflow processes, several studies
(
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
(ToWFnet) (
(P; T; F; F I; I; O) with:
net N is a tuple
interfaces that are responsible of messages receiving from other processes: I = ;.
interfaces responsible of messages sending to other partners: O = ;.
transitions of different processes.
F ((P [ I) relation, F I : T ! Q+ Q+ [ f1g is the function which associates to 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 the minimal and the maximal firing time respectively, 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 8q 2 (P [ I [ O) n fpg.
A transition t is 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) = ft0 2 En(M 0)jt0 = t _ :M t + t0g.
When a transition t becomes enabled, its firing interval is set to its static firing interval F I(t). The upper and lower 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.
the process that is modeled with ToWF-net after the occurrence of an event. Formally, we characterize a state in a ToWF-net by a pair (M; Int) where:
Int is a firing interval function, Int : En(M ) ! Q+ Q+ [ f1g. 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) 8t 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, we define the transition relation between states s1 = (M1; Int1) and s2 = (M2; Int2) by !d in case of time progression and by !t in case of a firing. We explicit in the following the conditions of state evolution and how to compute the resulting state after an event occurrence.
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 8t0
2 En(M2),
F I(t0) if t0 2 N En(M1; t) Int1(t0) otherwise Int2(t0) = 2. s1 !d s2 8d 2 R if and only if state s2 is reachable from s1 by a time progression with d time units, i.e. minInt1(t) + d M2 = M1, and
maxF I(t), 8t 2 En(M1), Int2(t) = [M ax(0; minInt1(t) d); maxInt1(t) d] We can now define the semantics of a ToWF-net N by a transition system (S; s0; !) with S the set of all the reachable states from the initial state s0 by ! the transition relation defined above.
We present in the following subsection some results of reachability analysis of ToWF-nets composition.
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.
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 = fsjs0 ! sg is the set of reachable states of the model, and ! is the reflexive and transitive closure of !.
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) 8t 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) (
bij i; j 2 [0::n]; bij 2 Q 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 (
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 than other specific properties.
Indeed, we focus in this section on the formal
verification of compatibility properties of ToWF-nets
as an extension of our results of compatibility
analysis while abstracting time information (
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 j :' j ' ^ ' j A(' UI ')j 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. (
The formal semantics of TCTL is given by the satisfaction relation defined as follows:
M, s 2 false, 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) 9r 2 I, M, ^(r) and 80 r0 r M, ^(r0) ', M, s 9('[I ) iff 9 2 (s) 9r 2 I, M, ^(r) and 80 r0 r M, ^(r0) ', When interval I is omitted, its value is by default [0; 1[.
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
PSPACEcomplete for bounded Petri nets (
The authors of (
defined inductively by: TPN-TCTL ::= false j ' j :' j ' _ E'UI j A'UI
j ' ^ j ' ) j j EGI ' j AGI ' j AFI ' j EFI ' j AG( 1 ) AF[0;d] 2).
Where ' and
2 TPN-TCTL, I = [a; b] or [a; b[ with a 2 N and b 2 N [ f1g.
1 and 2 are propositions on markings. 8G( 1 ) 8F[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 TPN-TCTL property: TPN-TCTLRomeo = E(p)U [a; b](q) j A(p)U [a; b](q) j EF [a; b](p) j AF [a; b](p) j EG[a; b](p) j AG[a; b](p) j EF [a; b](p) j (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)f+; gb M (j)f<; <=; >; >=; =gk j deadlock j bounded(k) j p and q j p or q j p ) q j 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 iff whenever p holds eventually q will hold as well in [0; b] time units.
In a composition of two or more processes, the correctness of the composite process refers in general to the compatibility of the different processes. From a behavioral point of view, the involved processes are compatible if they can interact properly. This means that composite process does not suffer from any deadlock problem. There is a distinction between syntactic compatibility which refer to the conformance of interfaces (number of interfaces, names, input, ouptut, etc.) and semantic compatibility which refer to the absence of deadlocks in the global system. In this paper, we focus only on defining and verifying the semantic compatibility. Before this, let us characterize the composite system obtained by superposing a number of ToWF-nets which are supposed syntactically compatible. The composite net N of nbX ToWF-nets N1... NnbX consists of all ToWF-nets sharing interface places. In this composite net, every input interface of a TWFnet has to be an output interface place of another TWF-net of N . Trivially, N form a time Petri net with nbX output places and nbX input places. The initial marking of N is M0 = Psn=bX1 is.
In (
In order to relax this definition, we propose different categories of the compatibility property.
Partial compatibility: A composite net N satisfies the partial compatibility if it is deadlock-free. Total Compatibility: A composite net N is totally compatible if it is deadlock-free and furthermore, the overall process terminates properly.
Perfect compatibility: A composite net N is perfectly compatible if it is totally compatible and the deadline constraints are satisfied.
Incompatibility: A composite net N is incompatible if it is neither partially nor totally compatible. We focus in what follows on formulating the four types of compatibility properties. Let us consider the following notation: nbX: the number of processes; nbp: the number of places in a given process; nbi: the number of interface places in a composition; is: the input place of the process number s. fs: the output place of the process number s.
Partial compatibility of nbX processes refers to the absence of deadlock in their composition. A net is deadlock-free if and only if there is at least a transition allowed in every marking except the final one Mfin which refer to the marking of all the final places fs (s = 1::nbX). This property is expressed as follows:
8M 2 [M0i, Mfin 2 [M i Logically, this deadlock-freeness property can be expressed as follows: "for all the executions made possible from the initial state, no deadlock is encountered until the final state is reached". The final state is characterized by the marking of the final places. Then, we can express the partial compatibility by the following TCTL formula: AG[0;1[((not M F ) ) not deadlock) In this formula, deadlock is a proposition supposed to return true if and only if there is no enabled transition in the current state. M F is a proposition on marking Mfin assuring that each final place is marked with at least one token.
M F = nbX ^ M (fs) >= 1 s=1 Here we check only the marking of final places.
The proper termination of a process refers to check if this latter complete its execution in any case, and at the time of termination, all the places of the involved ToWF-nets are empty except the final places which must be marked with exactly one token. Hence, we have to check if there exists a marking M for which all the places are empty except the output ones. Formally, this property can be expressed as follows: M (fs)
8M 2 [M0i : 1 8s 2 f1; ::; nbXg )
M = Psn=bX1 fs We can formulate the proper termination in TCTL as follows:
AF[0;1[ StrictM F With StrictM F a proposition on the marking with a token in every final place fs but no tokens in the other places including the interface ones.
nbX StrictM F = ^ s=1 nbip ( ^ (M (p) = 0) p=1 ^ (M (fs) = 1)) ^ nbi ( ^ M (Ii) = 0) i=1 where nbip is used to denote the number of places other than the final place in a process.
When we have a strict overall deadline that the system should respect, we can enforce the total compatibility by adding this constraint. We define, in this sense, the perfect compatibility which refers to both deadlock-freeness and proper termination while taking into account the deadline verification. Let us suppose that the deadline constraint is considered, this can be checked by verifying that a process has to terminate (reach its final state) in T m time units. Which lead to the expression of the proper termination within this delay as follows:
AF[0;T m] StrictM F Hence, these two TCTL formulas can be used to express the perfect compatibility of ToWF-nets composition:
AG[0;T m]((not M F ) AF[0;T m] StrictM F ) not deadlock)
The incompatibility is a situation in which neither deadlock-freeness nor proper termination is verified. In other words, a set of ToWF-nets are incompatible if all the possible executions don’t lead to final states of the different processes. We may distinguish here between strong incompatibility checked in the interval [0; 1[ and weak incompatibility which refers to incompatibility in a limited interval [a; b]. If we consider that the interval [x; y] may correspond to [0; 1[ or [a; b], the expression of the incompatibility in TCTL leads to the following formula:
AG[x;y]((not M F ))
We present in this subsection some results related
to the analysis of the compatibility and soundness
properties for a ToWF-nets composition. This
verification is ensured by Romeo (
We propose to study a simple composition of ToWFnets (figure 1). We can easily verify that no deadlock will be encountered until final places are marked. Then the partial compatibility is satisfied (see figure 2). However, the firings of transitions T4 and T5 of the second ToWF-net lead to two tokens in its final place f2; this violates the total compatibility property. In the figure 3, we show the result for this property and an execution trace. After that, we propose a correction in figure 4 for which the total compatibility is verified (see figure 5).
In this section, we tackle with a parametric quantitative analysis of the composition of ToWFnets. This suppose to consider k instances of each ToWF-nets ready to be executed.
For sake of covering the maximum number of real world processes, we tackle with time processes which share resource places. This places possess tokens in the beginning of each process and these tokens will be used and released after their use, i.e. at the end of execution, the resource places will regain their same initial markings.
For this, we define the time open WF-nets with shared resources (ToWFR-nets) which stand for a class of Petri nets dedicated to model workflow processes with: time delays, resource places as well as interface places.
(P; RP; T; F; RF; F I; I; O; WRP ; M0) with: tuple (P; T; F; F I; I; O) is a ToWF-net,
RF (RP for resources, T ) [ (T
WRP : RF 7! N is the weight function defining the weight of arcs linking the resource places. To ensure the use of resource places, we require: WRP (u) 18u 2 RF M0 is the initial marking: M0 = k:i + MRP where k is the number of tokens in the initial place i and MRP is the marking of resource places. For the interaction of ToWFR-nets, we use only interface places; resource places are used to model resources sharing between activities of the same process.
In the sequel, we will use these notations: IOj refers to interface place number j
RPj refers to resource place number j.
As an example of ToWFR-nets composition, we study a manufacturing lane of three machines which collaborate together to manufacture some product. The composite net describing the manufacturing workflow is given in figure 6.
In this example, each machine will be launched twice (2 tokens in each initial place ij ) and share an internal resource modeled by RPj with j the number of machines. The three machines communicate via the two interface places IO1 and IO2.
Now, to verify if the interacting ToWF-nets communicate correctly and if their collaboration process is sound, we propose to extend the above classes of compatibility properties with the consideration of the concurrent instances ready for execution.
We define the following formulas: the k-partial compatibility and the k-total compatibility. k-partial compatibility The k-partial compatibility refers to verify if all the instances of the involved processes terminate without encountering a deadlock. This is possible by extending the deadlock-freeness specified in the previous section with a test of the termination of the k instances. This can be specified by the following TCTL formula:
nbX AG[0; 1[(not( ^ (M (index_of _fs) >=
s=1 k)) => not deadlock) Where nbX is the number of involved processes
The figure 7 shows that the two-partial compatibility is guaranteed for the three machines example. The k-total compatibility refers to verify if all the instances of the involved processes terminate properly. This means that we have to verify if we reach the state in which final places have k tokens and resource places regain exactly their initial marking and all the other places are empty. This can be specified by the following TCTL formula: nbX AF [0; 1[( ^ (M (index_of _fs) =
s=1 mRPj ) ^ nbR ^ (M (index_of _RPj ) = k) ^ j=1 nbop ^ (M (index_of _Pj ) = 0)) j=1 Where nbX refers to the number of interacting processes, nbR refers to the number of resource places, mRPj refers to the initial marking of resource place RPj and nbop refers to the number of places which are neither final places nor resource places. For the three machines example (6) this formula is written in Romeo as follows:
AF [0; inf ](M (4) = 1 and M (7) = 1 and M (26) = 1 and M (27) = 1 and M (16) = 1 and M (3) = 1 and M (1) = and M (2) = 0 and M (5) = 0 and M (6) = 0 and M (8) = 0 and M (9) = 0 and M (10) = 0 and M (11) = 0 and M (12) = 0 and M (13) = 0 and M (14) = 0 and M (15) = 0 and M (17) = 0 and M (18) = 0 and M (19) = 0 and M (20) = 0 and M (21) = 0 and M (22) = 0 and M (23) = 0 and M (24) = 0 and M (25) = 0) The figure 8 shows that the two-total compatibility is guaranteed for the three machines example. After these tests, we highlight some results on the characterization of quantitative properties of ToWF-nets composition. Let us consider N the time workflow net obtained by composing the involved ToWF-nets and the adding of two special places pstart and pend and two transitions tstart and tend which connect respectively pstart to the the input places of the different ToWF-nets and the different final places to pend.
We can easily prove that if the involved ToWF-nets are totally compatible then N is sound. In addition if the ToWF-nets are k-totally compatible then N is ksound. But the reverse is incorrect, i.e. N is k-sound 9 the ToWF-nets are k-totally compatible.
Several works dealt with the analysis of compatibility
properties of processes modeled by open workflow
nets or by other formalisms. Wil M. P. van der Aalst
and al. (
Lucas Bordeaux and al. (
Wei Tan and al. (
While these approaches dealt with non time processes, we focused on those constrained by time information. To check the compatibility of interacting processes, we chose to extend oWF-nets with delays associated to activities. In addition, we were based on the formal verification in our approach. We mainly used the model checking formal method to check the compatibility classes of ToWF-nets, which shows a counter example in case a property is violated allowing thus to recognize and correct the eventual errors as early as possible.
Nowadays, technological progress plays a fundamental role in the optimization of production processes in different sectors, especially facing the varieties produced and the constraints of productivity, capability, quality and competitiveness. For this, a prior verification of such processes and their interaction is tremendous.
We proposed first in this paper a model for processes interaction based on Petri nets. Then, we studied the compatibility of these processes by model checking techniques. In particular, we applied a TCTL model checking of these properties and simulated some examples on the Romeo model checker. Finally, we enhanced these results by taking into account several instances ready for execution as well as a possibility of sharing resources. Hence, we introduced to parametric verification of interacting processes. In future, we propose to strengthen this parametric analysis of ToWF-nets and ToWFR-nets.