The composition of heterogeneous software components is required in many domains to build complex systems. However, such compositions raise mismatches between components such as unspecified messages. Checking compatibility for asynchronously communicating systems with unbounded channels is undecidable. In this paper, we propose a compatibility control approach based on a coverability product, which is a finite abstraction of the asynchronous products of I/O-transition systems. This coverability product is used to check UR-compatibility, without requiring a synchronizabity of the peers. We distinguish between messages brought by acyclic path and those brought by cycles. This allows us to overcome over-approximation for some arcs. Furthermore, we define relationships, called patterns, to check a good choreography between peers in terms of emission and reception activities.
Component-based development aims at facilitating the construction of very
complex applications by reusing and composing existing components. The assembly
of components offers a great potential for reducing cost and time to build
complex software systems and improving system maintainability and flexibility. A
software component is generally developed independently and is assembled with
other components, which have been designed separately, to create complex
systems. Normally glue code is written to realize such an assembly. Compatibility
checking is used to control if composed components can work together without
errors. This verification is very important for ensuring correct interaction
between components and may be done by using different formal models such as
interface automata, I/O-transition systems, -calcul, Petri nets and state
machines [
There are several incompatibility notions: (1) label incompatibility concerns
messages exchanged between components which can be handled differently. For
instance, messages are named differently, methods are called with parameters
which don’t match perfectly (incompatible types, different orders, ...) [
To deal with incompatible components, pessimistic and optimistic approaches
have been proposed. The pessimistic approach considers that two components
are compatible if they can always work together in any environment while, in
the optimistic approach, two components are compatible if they can be used
together in some helpful environment [
Components can interact synchronously or asynchronously. In synchronous
communications, a send action is a lock-step, since it is allowed only when the
receiver is ready to perform the corresponding reception. Thus, send and receive
actions are performed simultaneously. In asynchronous communications, a send
action is not a lock-step. The messages sent are added to the receiver buffers.
Such buffers may be ordered or unordered. Analyzing asynchronous
communicating components with unbounded buffers is a complex task, undecidable in
general [
Brand and Zafiropulo are among the first to have proposed works in the area of
service compatibility checking [
The works in [
Recently, Bouajjani and Emmi [
In [
Motivation
!a s0 s1
!b
s2
(a)
s0
0
?b
s0
1
?a
their emission. The peers are compatible with unordered queues but not with
FIFO queues. In Figure 1.b, peer 1 (resp. peer 2) sends message a (resp. b) and
loops infinitely by consuming b (resp. a) and then sending a (resp. b). All works
based on synchronizability property [
First we give the definition of an I/O-transition system.
Definition 1 An I/O-transition system A is a 4-tuple (SA; SAinit; A; A) such that:
2. SAinit SA a set of initial states. 3. A = AI [ AO [ H , where AI , input, output and internal actions.
AO and
AH are finite disjoint sets of In an I/O-transition system, each input (resp. output, internal) action is preceded by the symbol ? (resp. !, ;). A finite execution in an I/O-transition system is an alternating sequence of states and actions s0 a!1 s1 : : : a!n sn such that si ai+!1 si+1 2 A. For the sake of clarity, we suppose that SAinit is reduced to a single state. 4.2
The asynchronous product of I/O-transition systems with unbounded buffers
may be infinite. In this paper, we propose to build a finite coverability product,
inspired from the standard approach of constructing a coverability graph for P/T
nets [
In our approach, we distinguish between the message occurrences brought by elementary paths and those brought by cycles. The former are explicitly represented in the product, while the latter are abstracted by a set . Thus, gives the set of unbounded messages. In the sequel, we confuse between terms message and action.
Let A1 = (SA1 ; s0A1 ; A1 ; 1) and A2 = (SA2 ; s0A2 ; A2 ; A2 ) be two I/Otransition systems. Automata A1 and A2 fulfils the following conditions: AI1 \
AO2 = ; and AO1 \ AI2 = ;. Let = A1 [ A2 be the set of actions of A1 and A2.
a 7-tuple (V; 1; 2; ; M; ; v0). V is the set of nodes, with v0 2 V being the root. i (with i = 1;2) is a function from V to SAi . V V is the set of labelled arrows. M is a function from V to N, assigning an ordinary marking to every node. is a function from V to 2 giving, for a node v, the set of its infinite actions (messages).
A step of A1 A2 is either a step of A1 or A2. The following definitions are useful to build A1 A2. node v of A1
A2 iff 9s !a s0 2 Ai and i(v)=s and either: Definition 3 (Enabling condition) A state s of SAi , for i 2 f1; 2g, enables a – – or 2 f! ; ; g, =? ) (a 2
(v) _ M (v)(a) > 0 ).
M (u)(a) = M (v)(a) and (u) = (v).
2(u) = 2(v), 8a 2 ,
, denoted by u < v, iff 1(u) = 2(v), 2(u) = 2(v), 9a 2 , M (u)(a) < M (v)(a), 8b 2 , (M (u)(b) M (v)(b) or b 2 (u)) and (u) (v).
Given two I/O-transition systems A1 and A2, the algorithm 1 constructs the coverability product A1 A2. For the sake of clarity we present the product for two I/O-transition systems. However, the algorithm can be easily extended to n I/O-transition systems. Algorithm 1: Coverability graph construction [ fv !a wg end end
unprocessed [ fv0g ; 32 33 end /* This loop is repeated for each edge s !a s0 of A2 . unprocessed unprocessed n fvg ; */ */
The interleaving between some actions of A1 and A2 are not necessary for the properties we target (dealock and UR-reception). They only increase the size of A1 A2. For instance, from state s0 of Figure 1.c, message c is sent and then message a. These actions can be done by the left peer without any interaction with the right peer. Hence, they can be replaced by a single and an atomic action !ca. Furthermore, the path s0 !!c s1 !!a s0 is reduced to s0 !c!a s0. This transition produces one occurrence of message a and another of b. We can also reduce sequences of internal or/and emission actions. However, the reduction of a sequence sj ? 0a!0 : : : kak !1 sj+k of Ai, i 2 f1;2g, is not always possible. Conditions required to reduce a path are given below: 1. No interaction: 0; : : : k 1 2 f!;; g. 2. No intermediary branching states: 8j < h < j + k, sh is not a branching state. 3. Occurrence in an elementary cycle: Either all the arcs of the sequence are in an elementary cycle or all are not.
The first point states that there is no interaction between the peer and its correspondent, whereas the two other points allow to preserve the behavior of the peer.
and suppose that s2 is the initial state of the left peer. Only the left automaton can be reduced by replacing the edges s0 !!c s1 and s1 !!a s0 by s0 !c!a s0. The coverability product, constructed by Algorithm 1, is shown in Figure 2. Unbounded actions of a node v, (v) are given between brackets. The occurrences of actions brought by elementary path are explicitly represented. In the reachable state (s0;s00; a;fc;ag), say u, the current state 1(u) of the first (resp. 2(u) of the second) I/O-transition system is s0 (resp. s00). The marking M of u is reduced to one occurrence of a (M (u)(a)=1, M (u)(b)=0 and M (u)(c)=0) and (u) = fc;ag meaning that the occurrences a and c are potentially infinite.
arcs are represented by gray lines to highlight the over-approximation notion,which will be introduced in the following section.
Notation 1 A strongly connected component (scc) C of a graph G is a maximal set of nodes C SG, where SG is the set of nodes of graph G, such that for every pair of nodes u and v in C, there is a directed path from u to v and a directed path from v to u. A scc C composed of one node is said trivial, otherwise non trivial. A path or cycle in G is called elementary if no node occurs more than once. A cycle is called simple if no edge occurs more than once. A scc is terminal if it has no outgoing edge. Let be a sequence of transitions or an elementary cycle of A1 A2. #( ;!a) (resp. #( ;?a)) gives the number of occurrences !a (resp. ?a) in and #( ;a) represents #( ;!a) #( ;?a). ?a ?b !b !ca s0; s00; fc;a;bg
!ca ?c s0; s01; fc;a;bg ?b ?a
C1 s0; s02; b; fc;a;bg ?b s0; s02; fc;a;bg
!ca ?b !ca !ca !ca
cycle , denoted by ( ;!), corresponds to fa 2 j #( ;a) > 0g. A cycle may consume accumulated actions, those in ( ;?) = fa 2 j#( ;a) < 0g.
In Figure 2, each cycle labelled by !ca is an infinite producer of c and a (#( ;c) = 1 and #( ;a) = 1). Similarly, for instance, cycle =?c !b ?b ?a consumes actions c and a which are not produced by (#( ;c) = 1 and #( ;a) = 1) but accumulated by cycles labelled by !ca. 4.4
We give in Figure 3.b a part of the coverability product of peers in 3.a. In node v1, peer A2 does not block, since peer A1, at state s0, is able to provide messages a. Now consider the sequence v0 !!a v1 !!a v1 ?!a v2 !!b v3 ?!b v4. At the end of this sequence, peers A1 and A2 are in states s1 and s02, respectively. Observe that A2 waits indefinitely message a which will never be provided by peer A1. Indeed, at state s1, peer A1 cannot produce message a. Hence, node v4, contray to v1, is a potential deadlock for peer A2.
s0
?b s1 !a Both edges v1 ?!a v2 and v4 ?!a v5 are over-approximated. However, the first is always possible, whereas the second is only possible for some executions. An over-approximated edge v ?!a v0 deserves special attention, since, for some executions, node v0 is never reached. Hence, their presence makes A1 A2 not reliable. A loop v ?!a v is not considered as over-approximated even if M (v)(a) = 0.
In this section, we propose a technique aiming at discarding gradually the over-approximated status for some edges. Algorithm 2 summarises this technique. Its input is a strongly connected component C of A1 A2. The algorithm returns false whenever some edges remain over-approximated, otherwise it returns true. The algorithm uses the sets simpleCycles(C) and reliableCycles(C,v), with v a node of C. The former contains all simple cycles of C and the second is a subset of simpleCycles(C) where each cycle contains node v and is composed of non over-approximated edges only.
The algorithm builds a set of nodes called Vover. A node of Vover is an initial extremity of at least one over-approximated edge. The algorithm is iterative. At each step, Vover is computed. The over-approximated status of each edge v ?!a v0, with v 2 Vover is discarded whenever there is a reliable cycle 2reliableCycles(C,v) producing indefinitely action a, i.e. a 2 ( ;!). At the next step, Vover is updated, since some edges turn into non over-approximated. Hence, new cycles become reliable.
The termination of the algorithm is ensured since there is a finite number of simple cycles, actions and edges. The algorithm is applied to the strongly connected components of A1 A2. It is obvious that if the product contains no over-approximated edges, then it is reliable and can be used to check the free of deadlock and UR-compatibility properties.
Consider again the coverability product of Figure 2. Applying the precedent algorithm to non trivial scc (C1) induces the following steps. 1. Gray edges (over-approximated) of C1 compose Eover. Algorithm 2: dealOverapproxation
Data: a strongly connected components C of A1
Result: boolean 1 new =true; A2 2 Eover = fv ?!a v0 an edge of C s.t. M (v)(a) = 0 and v 6= v0g ;
/* Eover contains the set of over-approximated edges 3 8 2 simpleCycles(C), :visited = f alse ; 4 while new do */
Vover = fv a node Cj9v ?!a v0 2 Eoverg; new=f alse ; foreach v 2 Vover do actions = fa 2 ja 2 ( ;!) ^ 2 reliableCycles(C;v) ^ : :visitedg ; foreach 2 reliableCycles(C;v) do
:visited = true end foreach over-approximated edge e = v ?!a v0 do if a 2 actions then
Eover = Eover n feg ; new = true; 2. In the first iteration, Vover contains the three nodes of C1 which are initial extremities of gray arcs. A reliable simple cycle, labelled by !ca, loops around each node of Vover. Thus, the set of actions fc;ag is associated to each node of Vover. All gray edges are then removed from Eover. 3. In the second iteration, Vover is empty and there is no change about edge status, inducing the termination of the algorithm. The algorithm returns true.
Likewise, the algorithm 2 is applied to the other scc of A1 A2 depicted in Figure 2. We can easily see that the coverability product depicted in Figure 2 is free of deadlock. 5
In this section, we focus on the widely notion unspecified receptions U R. A set of peers is U R-compatible if they do not deadlock and each sent message by a peer is received by another one. Consider the peers given in Figure 1.c and consider s0 as initial state of the left peer. It is obvious that there are a good choreography and proper interactions between the peers, since the right peer requires an equality between messages a and c, a relation satisfied by the left peer of the Figure 1.c. However, when we add a cycle, for instance, s0 !!a s0 for the left peer, the equality relation between a and c is lost inducing a mess in the consumption activity. In this paper, we propose an approach to determine relationships between unbounded actions and use such relationships to check the U R compatibility through A1 A2. 5.1
In this paper, we suppose that a turn of any cycle may produce (or consume) at most one occurrence of a given action. In other terms, 1 #( ;a) 1 for any action a of any cycle of A1 A2.
Consider a non-trivial scc C of a free of deadlock coverability product. It is worth noting that, by construction, the set of unbounded actions is the same for any node of C; we use (C) to denote such a set. The relationships between unbounded actions within C consists to partition set (C) to P(C) = fP1; : : : ; Png such that for any node v of C, any cycle v ! v and any part Pj 2 P(C), the accumulated actions of (C) verify the following equality: a; b 2 Pj , #( ;a) = #( ; b). P(C) is called the pattern of C.
We inductively build P(C), by considering the elementary cycles of C. Initially, the partition associated with C is empty. At step i, a new partition is computed according to the partition in the previous step i 1 by considering a new elementary cycle of C. Cycle may alter the relationships between some actions. In other terms, it may change the relationships between the part’s elements of the partition computed in step i 1, since it brings some actions and consumes other actions, with the same rhythm. Thus, taking into account the restriction presented at the beginning of this section, each part P of the old partition is split into three subsets E, R and N .
– A subset E gathering actions of P produced by . Each action of E wins one occurrence for each turn of . – A subset R gathering actions of P consumed by . Each action of R loses one occurrence for each turn of .
– A subset N gathering actions of P which are not changed by .
Furthermore, the set E ( ; !) (resp. R ( ; ?)) whose actions don’t belong to any part of the old partition is added to the partition being computed. E (resp. R) constitutes a fresh equality relationship.
Example 2 Consider a partition Pi(C) = ffa;b;c;d;eg;ff;ggg, obtained at the ith iteration, and a new elementary cycle =!a !b ?b ?c !f ?e !h ?i?j, so: - ( ;!) = fa;f;hg, ( ;?) = fc;e;i;jg, Algorithm 3: Pattern computation - Partition obtained at the next iteration Pi+1(C) = ffag; fb;dg; fc;eg;ff g; fgg; fhg; fi;jgg.
Part fa;b;c;d;eg is split into three subsets, fag; fb;dg; fc;eg since #( ;a) = 1, #( ;b) = #( ;d) = 0 and #( ;c) = #( ;e) = 1, idem for the part ff;gg. Cycle brings new actions, h 2 ( ;!) and i; j 2 ( ;?), inducing two parts fhg, fi;jg in Pi+1(C). It is worth noting that cycle has broken the equality of a with the other actions of its part in Pi(C), keeps an equality between b and d (resp. c and e) and so on. 5.2
The pattern of a scc must C also take into account the elementary cycles of the ascendants scc of C. It is worth noting that the action occurrences, brought by elementary paths, are explicitly represented in the coverability product and are not included in the computation of the patterns of the scc. Consider again the coverability product of Figure 2, the pattern of scc C0 (resp. C1), computed in isolation is ffc; agg (resp. ffc; ag;fbgg). The pattern of C0 is preserved when considering the ascendant scc, idem for C1.
erability product if for any elementary cycle of C, ( ;?) 2 P(C).
Consider an element E 2 P(C). By construction, there is an equality relationship, in some nodes of A1 A2, between occurrences of actions of E. Any elementary cycle such that ( ;?) = E consumes, at each turn, a same number of elements of E preserving the relationship. Thus, the comsumption is in a step with the production rythm.
unique terminal Scc is P(C1) = ffc;ag; fbgg. There is a choreography compatibility within C1, since cycles of C1 fulfill definition 7. For instance, ( ;?) = fa;cg 2 P(C1) for cycle =?c !b ?a 2 C1, idem for ( ;?) = fbg 2 P(C1) for cycle =?b 2 C1. 5.3
The UR compatibility requires that each message sent is eventually received. To ensure that all sent messages are received, we must have in all terminal strongly connected components, cycles able to consume accumulated actions. These cycles are garbage collectors.
Definition 8 A cycle ( ;!) = ;.
of A1
A2 is a garbage collector iff: ( ;?) 6= ; and
A garbage collector is able to clean the actions ( ;?). In the other hand, the cycle does not produce residual messages. Consider again the coverability product of Figure 2. The cycle labelled by ?b is a garbage collector of action b, whereas the cycle labelled by ?c!b?b?a is a garbage collector of actions a and b. Proposition 1 Two automata A1 and A2 are UR-compatible if the coverability product A1 A2 is free of deadlock and for any terminal scc C of A1 A2 the following conditions hold: – There is a choreography compatibility within C. – For any node v of C and any action a of (v), there is a garbage collector of a.
– 8a 2 , 9 a node v of C, such that M (v)(a) = 0.
Proof. The first point states that there are proper interactions between peers, while the second ensures that peers are able to clean the accumulated actions. Finally, the last point indicates that the peer’s buffers always reach a state where any action brought by an elementary path has been emptied.
The coverability product of Figure 2 holds the conditions of the previous proposition. Thus, the peers of example 1 are U R-compatible. 6
In this paper, we presented a new approach to check compatibility of asynchronous communicating infinite systems, using unbounded and unordered buffers. We do not have any restrictions on the number of cycle iterations, size of buffers nor on number of components. Our main result is that our approach does not require any synchronizability property. In our approach, we proposed a coverability product by constructing a finite state space. We define the concept of patterns associated with messages occurring in the cycles of a strongly connected component. These patterns are jointly used with the covering graph to check the UR-compatibility of the components. The patterns allow to make an underlying analysis of strongly connected components. Thus, they show if there is a good choreography between components.
We have implemented our approach, which is under experimentation as future work, we aim to consider systems with FIFO unbounded buffers. This work could be a promising base to tackle with infinite systems.