The design and verification of an asynchronous communicating system can be very complex. In this paper we focus on weak termination: in each reachable state, the system has the option to eventually terminate. We present a component framework and construction method that guarantees weak termination. In the framework, communication between components is modeled by portnets, a special class of workflow nets. A basic component defines the orchestration of the portnets. For weak termination, the orchestration should accord to each of the portnets. A composite component is built from basic components that offer some service via a portnet. We provide sufficient conditions to guarantee weak termination for composite components. Furthermore, we present a refinement-based construction procedure to derive a weakly terminating composite from an architectural diagram of the system.
The class of asynchronous communicating systems encompasses a wide range of software systems that include information systems, embedded systems, grid computing systems, etc. The distributed nature and growing complexity of these systems warrant the need for a component based development (CBD) approach with support for formal analysis techniques. The central idea in the design of such systems involves the construction of complex systems by assembling components while guaranteeing certain properties.
Over the past years, different formal models supporting component based
development have been proposed, like Cadena [
The weak termination property states that in each reachable state of the
system, the system always has the possibility to reach a final state.
Generalized soundness [
Components are loosely coupled. As a consequence, their composition
introduces a high degree of concurrency, and thus a state space explosion. In [
In this paper, we present a component framework to construct a network of
asynchronously communicating components that guarantees weak termination.
The framework supports a best practice in communication protocol design:
communication between two components is first modeled as a state machine. Then,
each transition is assigned to one of the components, such that if any two
transitions are in conflict, these transitions are designated to the same component.
Then, the state machine is duplicated for each of the components. If a transition
is assigned to that component, it sends a message; the corresponding transition
of the other component receives this message. Such a net is called a portnet. In
this way, a component consists of a set of portnets defining its behavior with
the environment. A component needs to orchestrate all its portnets, such that
for each component it communicates with, it acts as the corresponding portnet.
This requirement is similar to the condition imposed by choreography standards
like WS-CDL [
The orchestration of a component may nest portnets. To resemble this in
the architecture, we introduce a simple architectural diagram. Furthermore, we
study the behavior of an arbitrary composition of components and give sufficient
conditions to guarantee weak termination. We also present a construction
procedure based on the rules of [
Let S be a set. We denote the powerset by P(S). A bag over some set S is a function m : N → S, where N = {0, 1, 2, . . .} denotes the set of natural numbers. For s ∈ S, m(s) denotes the number of occurrences of s in m. We enumerate bags with square brackets, e.g. the bag m = [a2, b3] has an element a occurring twice and element b occurring thrice and all other elements have multiplicity zero. The set of all bags over S is denoted by B(S). We write [] for an empty bag and we use + and − for the sum of two bags and =, <, >, ≤, ≥ to element wise compare bags, which are defined in the standard way. A set can be seen as a multiset in which each element of the set occurs exactly once.
A Petri net is a tuple N = (P, T, F ), where P is the set of places; T is the set of transitions such that P ∩T = ∅ and F is the flow relation F ⊆ (P ×T )∪(T ×P ). We refer to elements from P ∪ T as nodes and elements from F as arcs. We denote the places of net N by PN , transitions as TN and similarly for other elements of the tuple. If the context is clear, we omit N in the subscript. We define the preset of a node n as N•n = {m|(m, n) ∈ F } and the postset as m•N = {n|(m, n) ∈ F }. We lift the notion of a preset and postset to sets: N•S = ∪s∈S N•s and SN• = ∪s∈S s•N for some set S ⊆ (P ∪ T ). If the context is clear, the subscript is omitted. A path ν in a Petri net N of length n ∈ N is a function ν : 1, . . . , n → (P ∪T ) such that (ν(i), ν(i+1)) ∈ F for all 1 ≤ i < n. We denote a path of length n by ν = hx1, . . . , xni where xi = ν(i) for all q ≤ i ≤ n. The set of all paths of a Petri net N is called the path space and denoted by P S(N ). Two Petri nets N and M are disjoint if (PN ∪ TN ) ∩ (PM ∪ TM ) = ∅. They are isomorphic, denoted by N ∼=ψ M if and only if a bijective function ψ : PN ∪ TN → PM ∪ TM exists such that PM = ψ(PN ), TM = ψ(TN ) and ∀(x, y) ∈ FN ⇔ (ψ(x), ψ(y)) ∈ FM . We write N ∼= M if a bijective function ψ exists such that N ∼=ψ M . The state of a Petri net N = (P, T, F ) is determined by its marking which represents the distribution of tokens over places of the net. A marking m of a Petri net N is a bag over its places P , i.e., m ∈ B(P ). A transition t ∈ T is enabled in m if and only if •t ≤ m. An enabled transition may fire which results in a new marking m0 = m − •t + t•, denoted by m →−t m0. We define the set of reachable markings of a Petri net N with marking m inductively by R(m) = {m} ∪ Sm→−tm0 R(m0). We define the net system of a Petri net N as a 3-tuple M = (N, m0, mf ), where m0 ∈ B(PN ) is the initial marking and mf ∈ B(PN ) is the final marking. The weak termination property for a net system M states that ∀m ∈ R(N, m0) : mf ∈ R(N, m), i.e. for all reachable markings from the initial marking the final marking is reachable. If a marking does not enable any transition in the net, it is called a dead marking. A place is called safe in a net system (N, m0, mf ) if ∀m ∈ R(N, m0), m(p) ≤ 1. Let N = (P, T, F ) be a Petri net. Net N is a workflow net (WFN) if there exists exactly one place i ∈ P with •i = ∅, called the initial place, one place f ∈ P with f • = ∅, called the final place, and all nodes n ∈ P ∪ T are on a path from i to f . The closure of a workflow net N is a net closure(N ) = (P, T ∪ {t¯}, F ∪ {(t¯, i), (f, t¯)}) such that t¯ ∈/ T and •i = f • = { }
t¯ . A WFN N weakly terminates if its net
system (N, [i], [f ]) weakly terminates. Note that in [
3
In this section, we introduce a compositional framework to describe component based systems built of components that are cyclic in their execution and react to inputs from their environment. The main concept of this framework is the notion of a component. A component may be basic or composite. A basic component provides a service and may in turn may use the services offered by other basic components. The interfaces of a basic component are modeled as a portnet. A portnet describes a communication protocol. Such a protocol describes all possible sequences of messages that may be exchanged during a service negotiation. A basic component is a closed ST-net providing some service by means of a sell side portnet and consuming services using buy side portnets from components that have a compatible sell side portnet. The sell side portnet of a basic component encapsulates all of its buy side portnets. Furthermore, we allow buy side portnets to be nested. A composite component is the composition of a set of pairwise composable basic components such that their dependency graph is acyclic.
A component is modeled as a Petri net. An activity within such a component is modeled by a transition. We distinguish between two types of places, namely internal places and interface places. An interface place is either an input place for one component or an output place for another component. An input place has an empty preset and an output place has an empty postset. All other places of a component are referred to as internal places. Tokens residing at interface places represent messages, otherwise they are simply state markers. Transitions are either internal transitions or interface transitions. An internal transition has no interface places in its preset and postset, whereas an interface transition has some interface places in its preset (then it is called a receive transition) or its postset (then it is called a send transition), but never in both. 3.1
Our component framework is based on open Petri nets (OPN) which are a subclass of classical Petri nets. OPN are ideal to model communicating systems. This is because they have a distinguished set of interface places that represent the interfaces of the net. A direct consequence of the interaction of an OPN with its environment results in tokens being exchanged between these places. Furthermore, we add structural constraints to derive subclasses of an OPN. A subworkflow net is a OWN that is a subnet of an OPN.
is defined as N = (P, I, O, T, F, i, f ), where (1) P is the set of internal places; (2) I is the set of input places with •I = ∅; (3) O is the set of output places with O• = ∅; (4) T is the set of transitions; (5) the sets P , I, O and T are pairwise disjoint; (6) i ⊆ P is the set of initial places; (7) f ⊆ P is the set of final places ; (8) ∀t ∈ T : •t ∩ I 6= ∅ ⇒ t• ∩ O = ∅ ∧ t• ∩ O 6= ∅ ⇒ •t ∩ I = ∅; and ((P ∪ I ∪ O, T, F ), i, f ) is the net system. We refer to the set I ∪ O as the interface places of the net. The skeleton of N is a Petri net defined as skeleton(N ) = (P, T, F 0), where F 0 = F ∩ ((P × T ) ∪ (T × P )). The skeleton system is defined as (P, T, F 0, i, f ).
If skeleton(N ) is a WFN then N is called a open workflow net (OWN) . If skeleton(N ) is a S-WFN then N is called a state machine open workflow net (S-OWN). If skeleton(N ) is a T-WFN then N is called a marked graph open workflow net (T-OWN) . If skeleton(N ) is a ST-net then N is called a ST open workflow net (ST-OWN) .
net of N denoted by M v N if and only if PM ⊆ PN , TM ⊆ TN , FM ⊆ FN , IM ⊆ IN , OM ⊆ ON , N•(TM ∪ OM ∪ PM \ {iM })∪(TM ∪ IM ∪ PM \ {fM })•N ⊆ (TM ∪ PM ∪ IM ∪ OM ).
The transitions of an open Petri net are distinguished into three categories depending on the direction of communication, namely send, receive and internal. A send transition contains an output place in its postset. A receive transition has an input place in its preset. A transition that does not send or receive is called an internal transition.
tion of a transition with respect to a place in an open Petri net N is a function λ : T → {send, receive, τ } defined as λ(t) = send ⇔ t• ∩ O 6= ∅ ∧ •t ∩ I = ∅; λ(t) = receive ⇔ •t ∩ I 6= ∅ ∧ t• ∩ O = ∅ and λ(t) = τ , otherwise, for all t ∈ T . We call a transition t ∈ T a communicating transition if and only if λ(t) 6= τ .
The refinement of safe places in a Petri net is a well known refinement step
and has been described in various contexts [
and an OWN M such that N and M are disjoint, a safe place p ∈ PN \ {n | iN (n) = fN (n) = 0} can be refined by M , resulting in an OPN N 0 = N p M = (P, I, O, T, F, i, f ) with P = (PN \ {p}) ∪ PM , I = IN ∪ IM , O = ON ∪ OM , T = TN ∪TM , F = (FN \((•p×{p})∪({p}×p•)))∪FM ∪(•p×{iM })∪({fM }×p•), i = iN , f = fN . We define the reduction of net N 0 by the subworkflow net M by reduce(N 0, M ) = N if and only if N 0 = N p M .
An OPN N is said to be reducible to another open Petri net N 0 if and only if successive applications of the reduce operation on net N results in the net N 0. Note that we restrict the definition to reductions only by the class of ST-net, since this is the inherent structure of all nets in this component framework. Note that this relation is a preorder.
is reducible to N 0 denoted by N N 0 if and only if N = N 0 ∨ ∃M : M is a ST-OWN ∧ (M 6= N ) ∧ (M v N ) ∧ reduce(N, M ) N 0.
Unlike in an OPN, interfaces in our component framework are more than just a set of interface places acting as message buffers. An interface is determined by a Petri net with a distinguished set of interface places, called the portnet. A portnet defines the communication protocol which specifies all acceptable sequences of messages that are permitted to be exchanged over the portnet.
A portnet is an S-OWN with structural constraints on the relation between transitions and interface places and paths through it. In a portnet, each interface place is connected to exactly one transition, and each transition is connected to exactly one interface place. Secondly, a portnet must satisfy the leg property. A path in a portnet is called a leg if it is a path from a split to a join. We also consider the initial place as a split and the final place as a join. The leg property requires every leg in a portnet to have at least two transitions with different directions of communication. Lastly, a portnet must satisfy the choice property, which requires all transitions belonging to the postset of a place to have the same direction of communication.
– ∀t ∈ T : |(•t ∪ t•) ∩ (I ∪ O)| = 1; – ∀x ∈ I ∪ O : |•x ∪ x•| = 1; – (Leg property) ∀β = hp1, t1...tn−1, pni ∈ P S(C) : (|p1•| > 1 ∨ p1 = iN ) ∧ (|•pn| > 1 ∨ pn = fN ) : ∃t, t0 ∈ β : λ(t) 6= λ(t0). – (Choice property) ∀t1, t2 ∈ T : •t1 ∩ •t2 6= ∅ ⇒ λ(t1) = λ(t2).
We distinguish between two types of portnets: A sell side portnet advertises a service and needs a startup message and terminates after sending a result message. A buy side portnet consumes a service by sending a startup message and terminates after receiving the result message.
side portnet denoted by sell(C) if and only if ∀t ∈ iC • : λ(t) = receive ∧ ∀t ∈ •fC : λ(t) = send and we call Portnet C a buy side portnet denoted by buy(C) if and only if ∀t ∈ iC • : λ(t) = send ∧ ∀t ∈ •fC : λ(t) = receive.
Note that ¬sell(C) ⇔ buy(C). A component is an OPN with a set of portnets. Every communicating transition in a component belongs to a portnet. Furthermore, every portnet of a component is either already a subworkflow net or there exists a subworkflow net that can be reduced to the corresponding portnet.
– ∀t ∈ TN : λ(t) 6= τ ⇒ ∃C ∈ Γ : t ∈ TC – ∀C ∈ Γ : ∃N 0 : N 0 is an OWN : N 0 v N ∧ N 0 The set of all sell side portnets of a component is defined as: sellside((N, Γ )) = {C ∈ Γ | sell(C)} and the set of all buy side portnets of a component is defined as: buyside((N, Γ )) = {C ∈ Γ | buy(C)}.
and M such that N M . Then N is weakly terminating if and only if M is weakly terminating.
Portnets of a component may be nested in each other.
nets C1, C2 ∈ Γ . We say portnet C2 is nested in portnet C1 denoted by C2 CN C1 if and only if ∃M1, M2 : M2 v M1 v N ∧ M1 C1 ∧ M2 C2.
Two portnets are said to be compatible if their skeletons are isomorphic. Furthermore, the set of input places of one portnet must match the set of output places of the other portnet while preserving the relation with their associated transitions. Note that a portnet is not compatible with itself.
with respect to some bijective function φ : (PC1 ∪ TC1 ∪ IC1 ∪ OC1 ) → (PC2 ∪ TC2 ∪ IC2 ∪ OC2 ), denoted by C1 ,φ C2 if and only if : – skeleton(C1) ∼=φ skeleton(C2), – OC2 = φ(IC1 ), IC2 = φ(OC1 ), – ∀x ∈ IC1 , t ∈ TC1 : (x, t) ∈ FC1 ⇔ (φ(t), φ(x)) ∈ FC2 , – ∀x ∈ OC1 , t ∈ TC1 : (t, x) ∈ FC1 ⇔ (φ(x), φ(t)) ∈ FC2
Basic components are the building blocks of this component framework. The Petri net structure of a basic component is modeled as an ST-OWN with a closure transition. A basic component has one sell side portnet by means of which it provides a service. The sell side portnet may have zero or more nested buy side portnets. Furthermore, each interface place belongs to a unique portnet. Definition 11 (Basic component). A component B = (N, Γ ) is a basic component if and only if |iN | = |fN | = 1, N is the closure of an ST-OWN and the following conditions are met: – ∀x ∈ IN ∪ ON , ∃!C ∈ Γ : x ∈ IC ∪ OC ; – ∃C ∈ Γ : iC = iN ∧ fC = fN ∧ sellside(B) = {C}.
Corollary 12. Consider a basic component B = (N, Γ ) and a portnet C ∈ Γ : sell(C). Then N closure(C).
Note that the closure transition allows the basic component to handle more than one service request. Fig. 1 gives an example of a basic component M = (N, Γ ), where Γ = {S1, B1, B2} and S1 is a sell side portnet. The sell side portnet has two nested buy side portnets: B1 CN S1 and B2 CN S1. Net N contains a subworkflow net with initial place q and final place q0. This subworkflow net can be reduced by nets B1 and B2. We refer to the resulting net as an orchestration net. Such a net provides the logic behind the order of invocation of the different buy side portnets within a basic component.
Two components are said to be composable if and only if the only set of nodes they share are interface places and if this set is not empty, then either they have compatible portnets or they have identical buy side portnets. Note that we require unique sell side portnets.
Definition 13 (Composable components). Two components X = (N, ΓN ) and Y = (M, ΓM ) are composable denoted by composable(X, Y ) if and only if – (PN ∪ IN ∪ ON ∪ TN ) ∩ (PM ∪ IM ∪ OM ∪ TM ) = (ON ∪ IN ) ∩ (OM ∪ IM ); – ∀C1 ∈ ΓN , C2 ∈ ΓM : ((OC2 ∩ IC1 ) ∪ (OC1 ∩ IC2 ) 6= ∅ ⇒ C1 , C2) ∧ ((IC1 ∩ IC2 ) ∪ (OC1 ∩ OC2 ) 6= ∅ ⇒ C1 =∼ C2 ∧ buy(C1)).
A composition of a set of pairwise composable components is almost a pairwise union of the tuples of this set, except that the interface places belonging to pairs of compatible portnets, now become the internal places of this composition. Furthermore, the set of portnets of this composition is the set of all incompatible portnets. We extend the composition operation to portnets by treating portnets as components. This is possible in the following way: Consider a portnet C, then this portnet is also a component (C, {C}).
of pairwise composable components is denoted by comp(S) = (N, Γ ), where N = (PN , IN , ON , TN , FN , iN , fN ) such that – PN = (S(X,Γ 0)∈S PX ) ∪ (S(X,Γ 0)∈S IX ∩ S(X,Γ 0)∈S OX ), – IN = S(X,Γ 0)∈S IX \ S(X,Γ 0)∈S OX , ON = S(X,Γ 0)∈S OX \ S(X,Γ 0)∈S IX , – TN = S(X,Γ 0)∈S TX , FN = S(X,Γ 0)∈S FX , – iN = S(X,Γ 0)∈S iX , fN = S(X,Γ 0)∈S fX , and – Γ = {C ∈ S(X,Γ 0)∈S Γ 0|∀C0 ∈ S(X,Γ 0)∈S Γ 0 : ¬(C , C0)}.
Note that the composition of one basic component is in fact the basic component itself. Furthermore, comp(S1 ∪ S2) 6= comp(S1 ∪ {comp(S2)}), where S1 and S2 are sets of pairwise composable basic components. 3.2
We now present a graphical notation to represent a composition of components
as an architectural diagram of the system. The diagram abstracts away from the
underlying control flow and focuses on the relationships between components and
the relationships between the portnets of a component. Components are depicted
by a rounded rectangle. The portnets of a basic component are represented by
a square. All entities are labeled. The dependency relation between a pair of
portnets belonging to different components is represented by a directed arrow
indicating the direction of communication initiation, i.e. from a buy side portnet
to a sell side portnet. A buy side portnet may have at most one outgoing directed
edge while a sell side portnet may have zero or more incoming directed edges. The
sell side portnet with zero incoming directed edges becomes the portnet of the
composition. The portnets of the composition are represented by extending the
portnet with a dotted line to the boundary of the composition. By the structure
of a component, we know that all the buy side portnets of a basic component
are nested within the sell side portnet. Furthermore, a buy side portnet may
nest one or more buy side portnets. We represent the nesting of portnets by a
dotted directed edge leading from the child to its parent. Note that the Service
Component Architecture assembly diagram [
In this section, we study the behavior of a composition of components. In particular, we are interested in weak termination of components, which we define on the skeleton system of the component.
weakly terminating if its skeleton system weakly terminates.
To prove weak termination for an arbitrary composition of components we
first show that the composition of a sell side portnet with a set of compatible
buy side portnets is weakly terminating. The crux of the proof relies on both the
leg property and the choice property. These properties ensure that every choice
and loop is properly communicated to the other compatible portnet, and once
the choice to provide a service to a buy side portnet has been made no other
buy side portnet can influence the service negotiation. The proof of the following
theorem can be found in [
all 1 ≤ i ≤ k, then comp({closure(A), B1, ..., Bk}) weakly terminates.
Weak termination for an arbitrary composition of portnets is not sufficient to guarantee weak termination for an arbitrary composition of components. To guarantee weak termination for a composition of components, we require the graph of the composition to be acyclic. This is because a cycle indicates a deadlock in the composition. In our framework, we call an acyclic composition of pairwise composable basic components a composite component. Note that we will use the shorthand D instead of D = (N, Γ ), D0 instead of D0 = (N 0, Γ 0) and so on, to denote a component without explicitly labeling the tuples. We first introduce the notion of a partner for a buy side portnet in a component, which is the component that provides the compatible sell side portnet.
nents, and the set B consisting of all buy-side portnets of the components of S, we define the function partner : S × B 9 S by ∀D, D0 ∈ S, ∀C ∈ B : D0 = partner(D, C) ⇔ ∃C0 ∈ Γ 0 : sell(C0) ∧ C , C0.
set of S of pairwise composable basic components. Let R ⊆ S × S be the relation such that ∀D, D0 ∈ S : (D, D0) ∈ R ⇒ ∃C ∈ Γ : D0 = partner(D, C). The composition is a composite component if and only if the transitive closure R∗ is irreflexive.
The result on weakly terminating composition of portnets in conjunction
with Lemma 8 allows us to prove that an arbitrary composite component weakly
terminates. Both the proof and an example of a deadlock in a cyclic composition
can be found in [
5
This section presents a construction method that derives a composition of basic components from an architectural diagram and ensures that the derived composition is weakly terminating. The construction method is based on place refinement and composition as defined in the previous sections.
The construction method starts with an architecture diagram of a composite component, like the one depicted in Fig. 2. To construct a basic component we require the three ingredients, namely a sell side portnet, a set of buy side portnets and a set of orchestration nets (ST-WFN). An orchestration net is used to elaborate the activities of a basic component by being able to introduce internal activities, concurrency and choice in a structured way. Furthermore, the places introduced by an orchestration net, may be refined with buy side portnets during construction, thereby allowing us to model both the choice of service invocations and concurrency in service invocations.
First, for each basic component in the diagram, design the sell side portnet. Next, for each basic component in the diagram, derive all its buy side portnets from existing compatible sell side portnets. Note that a buy side portnet may be derived from a sell side portnet by changing the direction of communication associated with each transition in the corresponding sell side portnet. Lastly, for each basic component in the diagram, design the necessary orchestration nets that will be required during the construction.
We may now convert all the sell side portnets into a basic component by introducing the closure transition. For each basic component, the architecture diagram gives the order of nesting of its portnets. Using this information, we may now start designing the control flow of a basic component by successive refinements of an existing internal place with either an orchestration net or a buy side portnet, until all the buy side portnets of the basic component have been added in the right order of nesting and the desired basic component has been constructed.
Construction method 1. Design an architecture diagram for an acyclic composition of basic components using the techniques of Sec. 3. 2. Design all the portnets and orchestration nets that we will need for this composition. 3. For each node in this architecture diagram select the corresponding sell side portnet and apply the closure operation. 4. For each basic component, repeat the following steps until in each basic component all the buy side portnets have been added in the right order of nesting, and the desired orchestration has been constructed: (a) If an orchestration needs to be added first, then choose an internal place and refine with the right orchestration net; (b) Otherwise, choose an internal place and refine with a buy side portnet in the order defined by the architectural diagram; 5. Compose the set of basic component using the composition operation.
5.1
For the construction of portnets, we extend the Jackson refinement rules R0, R1, R2, and R3 with interface places as depicted in Fig. 3. Note that rule R0 is a special case of the refinement rule of Def. 3. Rule R00 and R000 extend rule R0 such that the refined transition can have either the communication direction send or receive. The extensions of rule R3 maintains the leg property by only adding loops with different directions of communication. Similarly, Rule R2, which adds a choice to the net is extended such that the choice property is maintained. Rule R1 is extended to allow two way communication.
The construction of an orchestration net starts with a single place. By
applying the refinement rules of [
6
We will model the control flow of the navigation system on a mobile robot. The software system comprises of four main components: The user interface, the navigation system, the platform controller and the laser scan controller. The robot perceives its environment by means of a planar laser scanner. The laser scan controller provides the latest scan as a service. The platform controller is a composite component and provides two services (a) to set a desired velocity (b) queries on the latest odometry. The navigation system is capable of creating a map of its environment and localizing itself on this map using the current laser scan and odometry services. Furthermore, the navigation system can accept a waypoint and generate a sequence of velocity commands that drive the platform to this waypoint while avoiding obstacles. The user interface at the remote location allows an operator to visualize this map and give waypoint to the navigation system. While a waypoint is in progress an operator receives feedback on the progress of this goal. Once the robot has reached its waypoint, the operator is notified. An architecture of the system is presented in Fig. 2.
The navigation system is a composite component comprising of the navigation manager and planning. The latter is again a composite component and comprises of the global planner, the local planner and the mapping and localization system. The mapping and localization system is capable of generating a map and localizing itself using the services offered by the laser scan controller and platform controller. The global planner accepts a map and a waypoint goal and generates a global plan (trajectory) from the robot’s current location to the waypoint goal. The local planner accepts a map and a global plan and generates a collision free sequence of velocity commands that drive the robot to the desired waypoint goal. The local planner generates these sequence of velocity commands in a loop until the destination is reached or a valid plan could not be found. In each cycle, the local planner makes use of the mapping and localization system to check its current location and generates feedback on the progress of this goal. If the destination has arrived then this is notified and the planner terminates. If at any moment, a valid velocity command could not be found then this situation is notified and the planner terminates. The navigation manager provides the waypoint navigation as a service to the user interface by orchestrating the components of the navigation system in the right order. The Fig. 4 presents five portents and one orchestration net. From the architecture diagram in Fig. 2, we know portnet P 5 is nested in P 12 and all other buy side portnets are nested in the sell side portnet P 4. We may now apply the construction method to derive the navigation manager in the following way: (((closure(P 4) r2 O1) r4 P 11) r5 P 13) r1 (P 12 r3 P 5). 7
In this paper, we introduced a compositional component framework and a construction method to design the control flow of a network of components, while guaranteeing weak termination. The two main concepts of this framework are portnet and basic component. A portnet models the interface of a basic component as a state machine which describes the communication protocol underlying a service negotiation. A basic component provides a service by orchestrating its portnets in the right way. The weak termination property was then investigated by first considering compositions of portnets. It turns out that any pair of compatible portnets that satisfy the leg property and the choice property always weakly terminate. Furthermore, we prove that an acyclic composition of basic components also known as a composite component weakly terminates.
In [