\section{Example: Message Communication}
\label{eg1}
In this section, we present an example that illustrates how transitional-invariant lattice can be used to verify correctness of adaptation in the context of a message communication program. We first discuss the programming notation used to describe the system. We then describe the fault-intolerant message communication program and the FEC-based {\em proactive component}. Next, we discuss adaptation of adding a proactive component to the fault-intolerant message communication program. We then discuss (in Sect. \ref{eg2}) adaptation of replacing the proactive component with an acknowledgment-based {\em reactive component}.
\subsection{Programming Notation}
In this subsection, we discuss the programming notation we use to describe the system. For brevity, we express programs using guarded commands \cite{inv-dij,closure-arora,networkprotocol-gouda}. This gives a compact representation of the program defined in Sect. \ref{model} (in terms of state space and transitions). It is straightforward to translate from the compact representation of the program to its automata representation discussed in Sect. \ref{model} as we discuss in this subsection.
\noindent {\bf Program and process}. \ A program $\mathcal{P}$ is specified by a finite set of processes and channels. A process $p$ is specified by a set of variables and a finite set of {\em actions}. The processes in a program communicate with one another by sending and receiving messages over unbounded channels that connect the processes. A channel from process $p$ to process $q$ is denoted by a channel variable $C_{p,q}$, which is an unbounded queue. Only process $p$ can append an item of data to the rear of the queue $C_{p,q}$ and only process $q$ can delete an item at the head of the queue $C_{p,q}$. Each variable has a predefined nonempty domain. A state of a process is obtained by assigning each variable a value from its respective domain. The state of the channel connecting $p$ and $q$ is given by the value of the queue $C_{p, q}$. The state of the program is given by the state of all the processes and the channels. Thus, the state space of the program $\mathcal{P}$, $S(\mathcal{P})$, is the set of all possible states of $\mathcal{P}$. We use $s(x)$ to denote value of variable $x$ in state $s$, and $V(p)$ to denote the set of variables of process $p$. The state predicate of $\mathcal{P}$ is a boolean expression over process and channel variables.
Note that a state predicate may be characterized by the set of all states in which its boolean expression is true and, therefore, is a subset of the state space of the program.
\noindent {\bf Action}. \ An action of $p$ is uniquely identified by a name, and is of the form
\vspace*{-2mm}
\begin{center}
$\langle\textit{name}\rangle \ : \ \langle\textit{guard}\rangle \ \rightarrow \ \langle\textit{statement}\rangle$
\end{center}
\vspace*{-2mm}
A guard of each action is a boolean expression over the process and the channel variables. The statement of each action is such that its execution updates zero or more process or channel variables. The set of actions of the program $\mathcal{P}$, $\Sigma(\mathcal{P})$ is given by the set of names of all the actions of all the processes of $\mathcal{P}$. Each action of $p$ gives a set of transitions of the form $(s, \pi, s^\prime)$ such that the guard of action $\pi$ is true in state $s$ and execution of statement of $\pi$ in $s$ results in state $s^\prime$. Thus, the state-transition relation $\delta(\mathcal{P})$ is obtained from the set of actions of all the processes of $\mathcal{P}$.
% and/or sends one or more messages. A sending statement of $p$ is of the form $send_{p,q}$, which sends a message to $q$. The sending of a message from $p$ to $q$ is causes a message to be appended at the tail of the queue $C_{p,q}$. The receive of a message from $q$ by $p$ is denoted by removing a message from the head of the queue $C_{p,q}$.
%\noindent A {\em guard} is a combination of one or more of the following: a state predicate of $p$, or a receiving guard of $p$. A receiving guard of $p$ is of the form \verb+rcv+ $\langle\textit{message}\rangle$ \verb+from+ $\langle q\rangle$. The {\em statement} of an action updates zero or more variables and/or sends one or more messages. An action can be executed only if its guard evaluates to true. To execute an action, the statement of that action is executed atomically. A sending statement of $p$ is of the form \verb+send+ $\langle\textit{message}\rangle$ \verb+to+ $\langle q_1, ..., q_n \rangle$, which sends a message to zero or more processes $q_1, ..., q_n$. We say that an action of $p$ is enabled in a state of $\mathcal{P}$ iff its guard evaluates to true in that state.
\noindent {\bf Component and fraction}. \ A component is specified by a finite set of fractions that are involved in providing a common functionality. Intuitively, a component implements a part of the desired behavior of the system, such as some algorithm or protocol. A component fraction is specified by a set of variables and a finite set of actions that are associated with a single process. A component (respectively, fraction) is syntactically same as a program (respectively, process), with only difference that some variables of the component are designated as {\em input}, whose values are supplied by the program with which it is composed. The composition of the component and the program is the union of the variables and actions of the component and the program.
\noindent {\bf Adaptive action}. \ An adaptive action is a special type of action, which is identified by a unique name and is of the form
\begin{center}
$\langle\textit{name}\rangle \ : \ \langle\textit{guard}\rangle \ \rightarrow \ \mathit{TransformTo}(p^\prime, \Phi)$.
\end{center}
\noindent When the statement of the adaptive action is executed, the current process is replaced by $p^\prime$ and state-mapping $\Phi$ is used to initialize the variables of $p^\prime$. Each adaptive action $\pi_a$ gives a set of adaptive transitions of the form $(s, \pi_a, s^\prime)$ such that the guard of $\pi_a$ is true in state $s$ of process $p$ and execution of the statement of $\pi_a$ results in state $s^\prime = \Phi(s)$ of process $p^\prime$. The state mapping function $S_{\mathit{map}}(\Delta)$ is obtained from the set of all adaptive actions.
From modeling perspective, we consider that the adaptive action replaces the entire process, even if only a small part of it is actually changed. In actual implementation, the adaptive action can performed in various ways, such as blocking of some method, or loading/unloading of some class. However, from verification point of view it is only important to consider the effect of the adaptive action. Additionally, considering each adaptive action as a generic form of process replacement gives the developer freedom to implement the adaptive action based on the platform and the language used.
\noindent {\bf State mapping}. \ We define the following classes of state mapping, $\Phi$, that occur during atomic adaptation:
\begin{itemize}
\item {\em Identity mapping}. \ In identity mapping, the names and values of the variables remain the same. Formally, for a variable $y$ of $V(p^\prime)$, there exists a variable $y$ of $V(p)$ such that for all $s$, $(\Phi(s))(y) = s(y)$.
\item {\em Quasi mapping}. \ In quasi mapping, the name of the variable of the new process is different from that of the old process, though its value is same as the value of some equivalent variable in the old process state when the adaptive action is executed. Formally, for a variable $y$ of $V(p^\prime)$, there exists a variable $x$ of $V(p)$ such that for all $s$, $(\Phi(s))(y) = s(x)$.
\item {\em Initial mapping}. \ In initial mapping, the variables of the new process are initialized to some value as in the initial state of the new process. Formally, for a variable $y$ of $V(p^\prime)$, for all $s$, $(\Phi(s))(y) = y_0$, where $y_0 \in S_0(y)$ and $S_0(y)$ is the set of values from domain of $y$ that $y$ can take in the initial states of process $p^\prime$.
\item {\em Functional Mapping}. \ In functional mapping, the value of the variable of the new process is some function of the values of variables of the old process. Formally, for a variable $y$ of $V(p^\prime)$, for all $s$, $(\Phi(s))(y) = f(V(p))$.
\item {\em Arbitrary Mapping}. \ A special type of functional mapping is arbitrary mapping, where all variables of the new process are assigned some arbitrary value. Formally, for a variable $y$ of $V(p^\prime)$, for all $s$, $(\Phi(s))(y) = y_d$, where $y_d \in D(y)$ and $D(y)$ denotes the domain of variable $y$.
\item {\em Mixed Mapping}. \ Most mapping that occur in practice are mixed mapping, in which variables of the new process $V(p^\prime)$ are divided into disjoint sets, and one of the above mappings is associated with each set.
\end{itemize}
\noindent {\em Notation}. \ We use ``$.$'' to denote the {\em belongs to} relation. For example, if variable $v$ belongs to process $p$, it is denoted by $p.v$, and action $a$ of process $p$ is denoted by $p.a$. A process $p$ of program $\mathcal{P}$ is denoted by $\mathcal{P}.p$, and a fraction $i$ of component $C$ is denoted by $C.i$. For brevity, we avoid using belongs to relation if it is obvious from the context.
%%%%%
\subsection{Fault-Intolerant Communication Program}
\label{origProgram}
\noindent {\bf Specification of the communication program}. \ An infinite queue of messages at a sender process $s$ is to be sent to two receiver processes $r_1$ and $r_2$ via two unicast channels and copied in corresponding infinite queues at the receivers. Faults may cause loss of messages in the channel.
\input{code/orig_prog}
\noindent The message communication program is shown in Fig. \ref{orig_prog}. Only \texttt{send} and \texttt{receive} actions of the program are shown, since only those actions are considered for adaptations.
Processes $s$, $r_1$, and $r_2$ maintain queues $\mathit{sQ}$, $r_1.\mathit{rQ}$, and $r_2.\mathit{rQ}$ respectively. $\mathit{sQ}$ contains messages that $s$ needs to send to $r_1$ and $r_2$. The messages received by $r_i$ from $s$ are stored in $r_i.rQ$. Let $\mathit{mQ}$ be the queue of all messages to be sent. ($\mathit{mQ}$ is an auxiliary variable that is used only for the proof.) Initially, $\mathit{sQ}$ = $\mathit{mQ}$. The function \verb+head+$(\mathit{sQ})$ returns the message at the front of $\mathit{sQ}$, and \verb+head+$(\mathit{sQ}, k)$ returns $k$ messages from the front of $\mathit{sQ}$. The function \verb+type+$(C_{s, r})$ returns the type of message at the head of channel queue. The notation $\mathit{sQ} \circ d$ denotes the concatenation of $\mathit{sQ}$ and $\langle d\rangle$.
\noindent {\bf Invariant}. \ The invariant of the communication program is $S_P = S1 \wedge S2$, where \\
{\small $S1 = \forall i:(m_i \in r_1.\mathit{rQ} \vee m_i \in r_2.\mathit{rQ}) \Rightarrow m_i \in \mathit{mQ}$}, and \\
{\small $S2 = \forall i:m_i \in \mathit{mQ} \Rightarrow (m_i \in \mathit{sQ} \veebar ((m_i \in C_{s, r_1} \veebar m_i \in r_1.\mathit{rQ}) \wedge (m_i \in C_{s, r_2} \veebar m_i \in r_2.\mathit{rQ})))$}.
\noindent In the above invariant, $S1$ indicates that messages received by the receivers are sent by the sender. $S2$ indicates that a message $m_i$ is not yet sent by the sender, or it is in the channel, or it is already received by the receiver, all exclusive.
\noindent {\em Notation}. \ The symbol $\veebar$ denotes {\em exactly one} operator, i.e. $x \veebar y \veebar z$ implies exactly one of $x$, $y$ and $z$ is true.
%%%%%
\subsection{Proactive Component}
\label{fecComponent}
The proactive component sends extra messages to the receiver, which the receiver can use to recover from lost messages. It consists of two types of fractions: encoder and decoder. The encoder fraction is added at the sender process and the decoder fraction is added at the receiver process. The encoder takes $(n-k)$ data packets and encodes them to add $k$ parity packets. It then sends the group of $n$ (data and parity) packets. The decoder needs to receive at least $(n-k)$ packets of a group to decode all the data packets. This component provides tolerance to certain message loss faults (discussed in Sect. \ref{eg2}).
\input{code/fecComp}
Fig. \ref{fecComp} shows the abstract version of the proactive component. The encoder and decoder fractions of the component are shown. The encoder fraction consists of two actions: \texttt{encode} and \texttt{fec\_send}. The decoder consists of two actions: \texttt{decode} and \texttt{fec\_receive}. These fractions are composed with the process that will use them. The composition of fraction and process is done by union, which is equivalent to appending the actions of the fraction and the process. We assume that appropriate renaming is performed so that there are no inconsistencies in definitions of the variables of the fractions and the processes. The message communication program composed with the proactive component is shown in Fig. \ref{fec_orig}.
\input{code/fec_orig}
\noindent {\bf Specification of program using the proactive component}. \ Program using the proactive component satisfies the same specification as the communication program (cf. Sect. \ref{origProgram}).
%Additionally, it tolerates message loss faults $F1$ (cf. Fig. \ref{f1}).
\noindent {\bf Invariant}. \ The invariant of the program using the proactive component is $S_Q = S1 \wedge S_F$, where
\noindent {\small $S_F = \forall i: m_i \in \mathit{mQ} \Rightarrow (m_i \in \mathit{sQ} \ \veebar \ ((m_i \in r_1.\mathit{rQ} \ \veebar \ m_i \in \text{data}(\mathit{encQ} \cup C_{s, r_1} \cup r_1.\mathit{rbufQ})) \ \wedge \ (m_i \in r_2.\mathit{rQ} \ \veebar \ m_i \in \text{data}(\mathit{encQ} \cup C_{s, r_2} \cup r_2.\mathit{rbufQ}))))$}
\noindent We use the notation $m_i \in \text{data}(\text{encQ} \cup C_{s, r_1} \cup r_1.\mathit{rbufQ})$ to imply that message $m_i$ can be generated from the $\text{data}$ in $\{\text{encQ} \cup C_{s, r_1} \cup r_1.\mathit{rbufQ}\}$. In the above invariant, $S_F$ indicates that the message is either at the sender, or already received by the receiver, or it can be generated from the data in the channel and the buffers at the sender and the receiver.
%%%%%
\subsection{Adaptation: Addition of the Proactive Component}
\label{adaptProgram}
Given a program shown in Fig. \ref{orig_prog}, the adaptation of adding the proactive component converts the program to one shown in Fig. \ref{fec_orig}. We first need to have adapt-ready version of the program $\mathcal{P}_{\mathit{intol}}$ as shown in Fig. \ref{orig_progA}.
\input{code/orig_progA}
\noindent {\bf Specification during adaptation}. \ The specification during adaptation is that $S_1$ continues to be true during adaptation.
%Our adaptation of adding the proactive component is based on the Java implementation in \cite{kb03podsy}. We call the entity that performs the adaptation as {\em composer}. To add the proactive component this adaptation starts when the composer at the sender process traps the \texttt{send} method and blocks it. The composer at the receiver process replaces the \texttt{receive} method with the decoder fraction after the \texttt{send} method is blocked and channel from the sender to the receiver is empty. After the decoder is added at both the receivers, the encoder is added at the sender process by replacing the \texttt{send} method.
\input{code/addfecIP1}
We identify the intermediate programs during adaptation after each atomic adaptation. The execution of adaptive action $a_1$ in $\mathcal{P}_{a\text{-}\mathit{intol}}$ results in the intermediate program $\mathcal{P}_{a\text{-}ip_1}$ shown in Fig. \ref{eg1IP1}. $\mathcal{P}_{a\text{-}ip_1}$ does not send any packets, but the packets that are there in the channel can still be received by the receivers $r_1$ and $r_2$. In the execution of $\mathcal{P}_{a\text{-}ip_1}$ eventually all the packets in the channel are read and no new packets are added in the channel from sender to receiver. Thus, the guards of the adaptive actions $a_2$ and $a_3$ eventually get enabled. The transitional-invariant of $\mathcal{P}_{a\text{-}ip_1}$ is: $\mathit{TS}_1 = S_1 \wedge S_2$, where $S_1, S_2$ are as defined earlier in Section \ref{origProgram}.
\input{code/addfecIP2}
Since $a_1$ and $a_2$ occur independently, we consider both possible orderings among them. The execution of adaptive action $a_2$ in $\mathcal{P}_{a\text{-}ip_1}$ results in the intermediate program $\mathcal{P}_{a\text{-}ip_2}$ shown in Fig. \ref{eg1IP2}. In $\mathcal{P}_{a\text{-}ip_2}$, receiver $r_1$ has replaced its fraction, whereas receiver $r_2$ has not yet replaced its fraction and can receive any remaining packets in the channel from $s$ to $r_2$. Eventually, in the execution of $\mathcal{P}_{a\text{-}ip_2}$ the guard of adaptive action $a_3$ gets enabled and $a_3$ is executed resulting in the intermediate program $\mathcal{P}_{a\text{-}ip_4}$.
The transitional-invariant of $\mathcal{P}_{a\text{-}ip_2}$ is $\mathit{TS}_2 = S_1 \wedge S_3$, where \\
{\small $S_3 = \forall i:m_i \in \mathit{mQ} \Rightarrow (m_i \in \mathit{sQ} \veebar ((m_i \in r_1.\mathit{rQ}) \wedge (m_i \in C_{s, r_2} \veebar m_i \in r_2.\mathit{rQ})) \wedge \text{isEmpty}(C_{s, r_1})=true \wedge \text{isEmpty}(r_1.\mathit{rbufQ})=true \wedge r_1.p = 0)$}.
\input{code/addfecIP3}
The execution of adaptive action $a_3$ in $\mathcal{P}_{a\text{-}ip_1}$ results in the intermediate program $\mathcal{P}_{a\text{-}ip_3}$ shown in Fig. \ref{eg1IP3}. In $\mathcal{P}_{a\text{-}ip_3}$, receiver $r_2$ has replaced its fraction, whereas receiver $r_1$ has not yet replaced its fraction and can receive any remaining packets in the channel from $s$ to $r_1$. Eventually, in the execution of $\mathcal{P}_{a\text{-}ip_3}$ the guard of adaptive action $a_2$ gets enabled and $a_2$ is executed resulting in intermediate program $\mathcal{P}_{a\text{-}ip_4}$.
The transitional-invariant of $\mathcal{P}_{a\text{-}ip_3}$ is $\mathit{TS}_3 = S_1 \wedge S_4$, where \\
{\small $S_4 = \forall i:m_i \in \mathit{mQ} \Rightarrow (m_i \in \mathit{sQ} \veebar ((m_i \in r_2.\mathit{rQ}) \wedge (m_i \in C_{s, r_1} \veebar m_i \in r_1.\mathit{rQ})) \wedge \text{isEmpty}(C_{s, r_2})=true \wedge \text{isEmpty}(r_2.\mathit{rbufQ})=true \wedge r_2.p = 0)$}.
\input{code/addfecIP4}
In the intermediate program $\mathcal{P}_{a\text{-}ip_4}$ shown in Fig. \ref{eg1IP4}, only the adaptive action $a_4$ is enabled, and execution of $a_4$ results in the new program $\mathcal{P}_{\mathit{fec}}$. The transitional-invariant of $\mathcal{P}_{a\text{-}ip_4}$ is $\mathit{TS}_4 = S_1 \wedge S_5$, where \\
{\small $S_5 = \forall i:m_i \in \mathit{mQ} \Rightarrow (m_i \in \mathit{sQ} \ \veebar \ (m_i \in r_1.\mathit{rQ} \ \wedge \ m_i \in r_2.\mathit{rQ})) \ \wedge \ \text{isEmpty}(C_{s, r_1})=true \ \wedge \ \text{isEmpty}(r_1.\mathit{rbufQ})=true \ \wedge \ r_1.p = 0 \ \wedge \ \text{isEmpty}(C_{s, r_2})=true \ \wedge \ \text{isEmpty}(r_2.\mathit{rbufQ})=true \ \wedge \ r_2.p = 0$}.
{\bf State mapping}. \ The state mapping for each adaptive action is shown in Table \ref{stateMappingEg1}. Each adaptive action initializes the state of the new process when it is executed based on this mapping.
\begin{table}[hbt]
\scriptsize
\centering
\begin{tabular}{|c|c|p{2.2in}|} \hline
{\bf Mapping Function}& {\bf Process Affected}& \multicolumn{1}{c|}{\bf New State}\\\hline
$\Phi_{a_1}$ & $s$ & Identity mapping\\[.25mm]
%%
$\Phi_{a_2}$ & $r_1$ & $\{\mathit{rQ}, s\}$ - Identity mapping, \newline
$\{n, k, x, y, p, m, \mathit{rbufQ}\}$ - Initial mapping \\[.25mm]
%%
$\Phi_{a_3}$ & $r_2$ & $\{\mathit{rQ}, s\}$ - Identity mapping, \newline
$\{n, k, x, y, p, m, \mathit{rbufQ}\}$ - Initial mapping \\[.25mm]
%%
$\Phi_{a_4}$ & $s$ & $\{\mathit{sQ}, r_1, r_2\}$ - Identity mapping, \newline
$\{n, k, u, l, m, \mathit{encQ}\}$ - Initial mapping \\\hline
\end{tabular}
\vspace*{0.5mm}
\caption{\small State mapping for each adaptive action.}
\label{stateMappingEg1}
\end{table}
\begin{figure}[htb]
\centering\epsfig{file=a.eps}
\caption{\small Adaptation lattice for addition of proactive component.}
\label{a-lattice}
\end{figure}
Fig. \ref{a-lattice} shows the adaptation lattice for the adaptation of adding the proactive component.
{\bf Theorem 1.1}. \ {\it The adaptation lattice of Fig. \ref{a-lattice} is a transitional-invariant lattice for the adaptation of adding the proactive component. Hence, the adaptation is correct.} \qed