The objective of this appendix is to provide the properties of the Petri net encoding of a
ServiceTemplate (see Definition
8) that are needed to prove its safeness (see Proposition
1). First, since each node
\(N_i\) in a
ServiceTemplate
S can be in a unique state, exactly one of the internal places denoting its states contains one token, while the others contain no token. This holds at any given time, and thus in any marking that can be reached from the initial marking of the Petri net encoding of
\({\mathcal {Z}}_S\). In short, (i) each internal place of the net encoding a
ServiceTemplate contains at most one token. The same holds also for the open places modeling (ii) capabilities and (iii) requirements.
Let
S be a
ServiceTemplate and let
\({\mathcal {Z}}_S = \langle \mathcal {P}_S, I_S \rangle \), with
\(\mathcal {P}_S = \langle P_S, T_S, {\bullet }\cdot , {\cdot \bullet }, M_0 \rangle \), be the Petri net encoding of
S. Let also
\(M\) be a marking reachable from the initial marking
\(M_0\) of
\({\mathcal {Z}}_S\). For each node
\(N_i = \langle S_{N_i}, R_{N_i}, C_{N_i}, O_{N_i}, \mathcal {M}_{N_i} \rangle \) (with
\(\mathcal {M}_{N_i} = \langle \overline{s}, \rho , \gamma , \tau \rangle \)) in
S, the following properties hold:
(i)
\( \exists s' \in S_{N_i}. M(s') = 1 ~\wedge ~ \forall s \in S_{N_i} . s \ne s' \Rightarrow M(s) = 0 \) or, equivalently:
$$\begin{aligned} \Sigma _{s \in S_{N_i}} M(s) = 1 \end{aligned}$$
(ii)
Let
s be the current state of a node
\(N_i\) (i.e.
\(s \in S_{N_i} \wedge M(s)=1\)). For any capability
\(c \in C_{N_i}\), the number of tokens in the open places
\(r_c\) and
c is:
$$\begin{aligned} c \notin \gamma (s)&\Leftrightarrow M(c) + M(r_c) = 0\\ c \in \gamma (s)&\Leftrightarrow M(c) + M(r_c) = 1 \end{aligned}$$
(iii)
Let
s be the current state of a node
\(N_i\) (i.e.
\(s \in S_{N_i} \wedge M(s)=1\)). For any requirement
\(r \in R_{N_i}\) bound to a capability
c (i.e.,
\(r \in b(c,S)\)), the number of tokens in the open places
r and
\(r_c\) is:
$$\begin{aligned} r \notin \rho (s)&\Leftrightarrow (M(r) = M(r_c) = 0) \vee (M(r) = M(r_c) = 1)\\ r \in \rho (s)&\Leftrightarrow M(r) = 0 \wedge M(r_c) = 1 \end{aligned}$$
\( \exists s' \in S_{N_i}. M(s') = 1 ~\wedge ~ \forall s \in S_{N_i} . s \ne s' \Rightarrow M(s) = 0 \) or, equivalently:
$$\begin{aligned} \Sigma _{s \in S_{N_i}} M(s) = 1 \end{aligned}$$
Let
s be the current state of a node
\(N_i\) (i.e.
\(s \in S_{N_i} \wedge M(s)=1\)). For any capability
\(c \in C_{N_i}\), the number of tokens in the open places
\(r_c\) and
c is:
$$\begin{aligned} c \notin \gamma (s)&\Leftrightarrow M(c) + M(r_c) = 0\\ c \in \gamma (s)&\Leftrightarrow M(c) + M(r_c) = 1 \end{aligned}$$
Let
s be the current state of a node
\(N_i\) (i.e.
\(s \in S_{N_i} \wedge M(s)=1\)). For any requirement
\(r \in R_{N_i}\) bound to a capability
c (i.e.,
\(r \in b(c,S)\)), the number of tokens in the open places
r and
\(r_c\) is:
$$\begin{aligned} r \notin \rho (s)&\Leftrightarrow (M(r) = M(r_c) = 0) \vee (M(r) = M(r_c) = 1)\\ r \in \rho (s)&\Leftrightarrow M(r) = 0 \wedge M(r_c) = 1 \end{aligned}$$
The proofs for (i), (ii), and (iii) are listed below.
(i)
For each node
\(N_i\), the places denoting its states are internal to
\({\mathcal {Z}}_S\). Hence, their input and output transitions are not changed by the merge process, which in turn means that only the net transitions (encoding the protocol transitions) of the same node
\(N_i\) can add/remove tokens to/from them. By construction, the above mentioned transitions always input exactly one token from an internal place and output exactly one token to an internal place (potentially the same). This guarantees that the total number of tokens in the internal places of a single node cannot change:
$$\begin{aligned} \Sigma _{s \in S_{N_i}} M(s) = \Sigma _{s \in S_{N_i}} M'(s), \end{aligned}$$
where
\(M'\) is a marking reached by firing a transition in
\(M\). The above, along with the fact that the initial marking
\(M_0\) of
\({\mathcal {Z}}_S\) includes a token only in the places denoting the initial states of the nodes in
S (i.e., for each node
\(N_i\),
\(\Sigma _{s \in S_{N_i}} M_0(s) = 1\)), implies that any sequence of firings starting from the initial marking will preserve exactly one token in the internal places denoting the states of each node.
(ii)
First, we show that the property holds in the initial marking
\(M_0\) of
\({\mathcal {Z}}_S\). According to the definition of management protocols (Definition
3),
\(\gamma (\overline{s}) = \varnothing \), which means that (in order for the property to hold) the initial marking
\(M_0\) of the open places must be empty (i.e., for each capability
c,
\(M(c) + M(r_c) = 0\)). This follows from the construction of
\({\mathcal {Z}}_S\) (Definition
8), thus the property holds for
\(M_0\). Since the property holds for the initial marking, we can prove that it holds for every reachable marking, by showing that no transition can invalidate the property. We will thus consider it as invariant. Consider the capability
c of a node
\(N_i\). The places mentioned in the property (i.e.,
c and
\(r_c\)) are connected to the
\(c_{\uparrow }\) and
\(c_{\downarrow }\) transitions, and to the transitions of
\(N_i\) that input/output a token to/from
c. These are the only transitions that might affect the invariant, since the transitions connected to the requirements managed by the controller of
c cannot change the marking of
c nor that of
\(r_c\). The
\(c_{\uparrow }\) and
\(c_{\downarrow }\) transitions cannot affect the invariant, since they do not change the total number of tokens in
c and
\(r_c\). This is because, whenever
\(c_{\uparrow }\) fires, it removes one token from
c, but it also adds one token to
\(r_c\) (and to all of the other
\(r_i\) places). Symmetrically, whenever
\(c_{\downarrow }\) fires, it removes one token from
\(r_c\) (and from each of the other
\(r_i\) places), but it also adds one token to
c. Thus, the only transitions that might invalidate the invariant are the transitions of the node
\(N_i\) that input/output one token to/from
c. Since all these transitions move a token from a state
s to a state
\(s'\), they can be classified as follows:
(a)
c is either provided in both
s and
\(s'\) or in neither of them (i.e.,
\(c \in \gamma (s) \cap \gamma (s') \vee c \notin \gamma (s) \cup \gamma (s')\));
(b)
c is provided in
\(s'\), but it is not provided in
s (i.e.,
\(c \in \gamma (s') - \gamma (s)\));
(c)
c is provided in
s, but it is not provided in
\(s'\) (i.e.,
\(c \in \gamma (s) - \gamma (s')\)).
Each of these cases is consistent with the property that we want to prove.
(a)
In the first case, transitions do not affect
c at all, as (by construction) they are not even connected to
c. They thus preserve the sum
\(M(c) + M(r_c)\), as well as the truth value of
\(c \in \gamma (\cdot )\).
(b)
In the second case, transitions lead to a state
\(s'\) such that
\(c \in \gamma (s')\), but they also add a token to
c. If the invariant held before the transition (i.e.,
\(M(c) + M(r_c) = 0\) with
\(M(s)=1 \wedge c \notin \gamma (s)\)), it also holds after the transition, because the sum becomes
\(M(c) + M(r_c) = 1\) with
\(M(s')=1 \wedge c \in \gamma (s)\).
(c)
The third case is precisely the opposite of the second one, since transitions lead to a state
\(s'\) such that
\(c \notin \gamma (s')\) and they remove a token from
c. If the invariant held before the transition (i.e.,
\(M(c) + M(r_c) = 1\) with
\(M(s)=1 \wedge c \in \gamma (s)\)), then it also holds after the transition. The sum indeed becomes
\(M(c) + M(r_c) = 1\) with
\(M(s')=1 \wedge c \notin \gamma (s)\).
In conclusion, since the invariant holds for
\(M_0\) and none of the transitions can invalidate it, by induction (over the length of a firing sequence) it holds for any reachable marking.
(iii)
The proof of the property follows the same line as the one for (ii). Namely, the property can be proved to hold for any reachable marking by induction over the length of a firing sequence, by showing that it holds for the initial marking
\(M_0\), and that none of the transitions can invalidate such property.
\(\square \)
For each node
\(N_i\), the places denoting its states are internal to
\({\mathcal {Z}}_S\). Hence, their input and output transitions are not changed by the merge process, which in turn means that only the net transitions (encoding the protocol transitions) of the same node
\(N_i\) can add/remove tokens to/from them. By construction, the above mentioned transitions always input exactly one token from an internal place and output exactly one token to an internal place (potentially the same). This guarantees that the total number of tokens in the internal places of a single node cannot change:
$$\begin{aligned} \Sigma _{s \in S_{N_i}} M(s) = \Sigma _{s \in S_{N_i}} M'(s), \end{aligned}$$
where
\(M'\) is a marking reached by firing a transition in
\(M\). The above, along with the fact that the initial marking
\(M_0\) of
\({\mathcal {Z}}_S\) includes a token only in the places denoting the initial states of the nodes in
S (i.e., for each node
\(N_i\),
\(\Sigma _{s \in S_{N_i}} M_0(s) = 1\)), implies that any sequence of firings starting from the initial marking will preserve exactly one token in the internal places denoting the states of each node.
First, we show that the property holds in the initial marking
\(M_0\) of
\({\mathcal {Z}}_S\). According to the definition of management protocols (Definition
3),
\(\gamma (\overline{s}) = \varnothing \), which means that (in order for the property to hold) the initial marking
\(M_0\) of the open places must be empty (i.e., for each capability
c,
\(M(c) + M(r_c) = 0\)). This follows from the construction of
\({\mathcal {Z}}_S\) (Definition
8), thus the property holds for
\(M_0\). Since the property holds for the initial marking, we can prove that it holds for every reachable marking, by showing that no transition can invalidate the property. We will thus consider it as invariant. Consider the capability
c of a node
\(N_i\). The places mentioned in the property (i.e.,
c and
\(r_c\)) are connected to the
\(c_{\uparrow }\) and
\(c_{\downarrow }\) transitions, and to the transitions of
\(N_i\) that input/output a token to/from
c. These are the only transitions that might affect the invariant, since the transitions connected to the requirements managed by the controller of
c cannot change the marking of
c nor that of
\(r_c\). The
\(c_{\uparrow }\) and
\(c_{\downarrow }\) transitions cannot affect the invariant, since they do not change the total number of tokens in
c and
\(r_c\). This is because, whenever
\(c_{\uparrow }\) fires, it removes one token from
c, but it also adds one token to
\(r_c\) (and to all of the other
\(r_i\) places). Symmetrically, whenever
\(c_{\downarrow }\) fires, it removes one token from
\(r_c\) (and from each of the other
\(r_i\) places), but it also adds one token to
c. Thus, the only transitions that might invalidate the invariant are the transitions of the node
\(N_i\) that input/output one token to/from
c. Since all these transitions move a token from a state
s to a state
\(s'\), they can be classified as follows:
(a)
c is either provided in both
s and
\(s'\) or in neither of them (i.e.,
\(c \in \gamma (s) \cap \gamma (s') \vee c \notin \gamma (s) \cup \gamma (s')\));
(b)
c is provided in
\(s'\), but it is not provided in
s (i.e.,
\(c \in \gamma (s') - \gamma (s)\));
(c)
c is provided in
s, but it is not provided in
\(s'\) (i.e.,
\(c \in \gamma (s) - \gamma (s')\)).
c is either provided in both
s and
\(s'\) or in neither of them (i.e.,
\(c \in \gamma (s) \cap \gamma (s') \vee c \notin \gamma (s) \cup \gamma (s')\));
c is provided in
\(s'\), but it is not provided in
s (i.e.,
\(c \in \gamma (s') - \gamma (s)\));
c is provided in
s, but it is not provided in
\(s'\) (i.e.,
\(c \in \gamma (s) - \gamma (s')\)).
Each of these cases is consistent with the property that we want to prove.
(a)
In the first case, transitions do not affect
c at all, as (by construction) they are not even connected to
c. They thus preserve the sum
\(M(c) + M(r_c)\), as well as the truth value of
\(c \in \gamma (\cdot )\).
(b)
In the second case, transitions lead to a state
\(s'\) such that
\(c \in \gamma (s')\), but they also add a token to
c. If the invariant held before the transition (i.e.,
\(M(c) + M(r_c) = 0\) with
\(M(s)=1 \wedge c \notin \gamma (s)\)), it also holds after the transition, because the sum becomes
\(M(c) + M(r_c) = 1\) with
\(M(s')=1 \wedge c \in \gamma (s)\).
(c)
The third case is precisely the opposite of the second one, since transitions lead to a state
\(s'\) such that
\(c \notin \gamma (s')\) and they remove a token from
c. If the invariant held before the transition (i.e.,
\(M(c) + M(r_c) = 1\) with
\(M(s)=1 \wedge c \in \gamma (s)\)), then it also holds after the transition. The sum indeed becomes
\(M(c) + M(r_c) = 1\) with
\(M(s')=1 \wedge c \notin \gamma (s)\).
In the first case, transitions do not affect
c at all, as (by construction) they are not even connected to
c. They thus preserve the sum
\(M(c) + M(r_c)\), as well as the truth value of
\(c \in \gamma (\cdot )\).
In the second case, transitions lead to a state
\(s'\) such that
\(c \in \gamma (s')\), but they also add a token to
c. If the invariant held before the transition (i.e.,
\(M(c) + M(r_c) = 0\) with
\(M(s)=1 \wedge c \notin \gamma (s)\)), it also holds after the transition, because the sum becomes
\(M(c) + M(r_c) = 1\) with
\(M(s')=1 \wedge c \in \gamma (s)\).
The third case is precisely the opposite of the second one, since transitions lead to a state
\(s'\) such that
\(c \notin \gamma (s')\) and they remove a token from
c. If the invariant held before the transition (i.e.,
\(M(c) + M(r_c) = 1\) with
\(M(s)=1 \wedge c \in \gamma (s)\)), then it also holds after the transition. The sum indeed becomes
\(M(c) + M(r_c) = 1\) with
\(M(s')=1 \wedge c \notin \gamma (s)\).
In conclusion, since the invariant holds for
\(M_0\) and none of the transitions can invalidate it, by induction (over the length of a firing sequence) it holds for any reachable marking.
The proof of the property follows the same line as the one for (ii). Namely, the property can be proved to hold for any reachable marking by induction over the length of a firing sequence, by showing that it holds for the initial marking
\(M_0\), and that none of the transitions can invalidate such property.
