\section{Verifying Adaptation in Presence of Faults \label{fsl-sec}}
In Sect. \ref{til-sec}, we defined transitional-invariant lattice that is used to verify correctness of adaptation in absence of faults. In this section, we define {\em transitional-faultspan lattice} to verify correctness of adaptation in presence of faults. We first introduce some terms that we use use in this section. These definitions are based on the previous work in \cite{closure-arora, multitolerance}. Next, we define {\em transitional-faultspan} and {\em transitional-faultspan lattice}. Using these definitions, we present an approach to prove correctness of adaptation in presence of faults.
\noindent {\bf Fault class}. \ Let $\Sigma_f$ be a set of fault actions. A fault class $F(\mathcal{A})$ for program $\mathcal{A}$ is a subset of the set $S(\mathcal{A}) \ \mathsf{x} \ \Sigma_f \ \mathsf{x} \ S(\mathcal{A})$. We use $\mathcal{A} [] F$ to denote the transitions obtained by taking the union of the transitions in $\delta(\mathcal{A})$ and the transitions in $F(\mathcal{A})$. A fault class $F(\Delta)$ for adaptation $\Delta$ is: \\
$\bigcup\limits_{\mathcal{A} \ \in \ \mathcal{I}} \{((\mathcal{A},s), \Sigma_f, (\mathcal{A},s^\prime)) \ | \ (s, \Sigma_f, s^\prime) \in F(\mathcal{A})\}$.
%{\em Assumption}. \ We assume finite occurrences of faults in any computation. This requirement is the same as that made in previous work \cite{dij, ak95, ag0, varghese-thesis} to ensure that eventually recovery can occur.
\noindent {\bf Fault-span}. \ A state predicate $T$ is a fault-span ($F$-span) of $\mathcal{A}$ from invariant $S$ iff $(i)$ $S \subseteq T$, and $(ii)$ $T$ is closed in $\mathcal{A} [] F$. Fault-span of a program identifies the set of states that a program can reach in presence of faults and asserts that the set of states is closed under the execution of program and fault actions.
\noindent {\bf Computation in presence of faults}. \ A computation of program $\mathcal{A}$ (respectively, adaptation $\Delta$) in presence of faults is a sequence of states $\sigma = \langle s_0, s_1, ...\rangle$ satisfying following conditions:
\begin{itemize}
\item For first state $s_0$ in $\sigma$, $s_0 \in S_0 (\mathcal{P})$ (respectively, $S_0(\Delta)$)
\item If $\sigma$ is infinite then $\forall j: j > 0: (\exists \pi::(s_{j-1}, \pi, s_j) \in \delta(\mathcal{A}) \cup F(\mathcal{A}))$ (respectively, $\delta(\Delta) \cup F(\Delta)$)
\item If $\sigma$ is finite and terminates in state $s_l$, then there does not exist state $s$ for all $\pi$ such that $(s_l, \pi, s) \in \delta(\mathcal{A})$ (respectively, $\delta(\Delta)$), and $\forall j: j > 0: (\exists \pi::(s_{j-1}, \pi, s_j) \in \delta(\mathcal{A}))$ (respectively, $\delta(\Delta)$)
\item $\exists n : n \geq 0 : (\forall j : j > n : (\exists \pi::(s_{j-1}, \pi, s_j) \in \delta(\mathcal{A}))$ (respectively, $\delta(\Delta)$)
\end{itemize}
The second requirement captures that in each step, either a program (respectively, program or adaptive) transition or a fault transition is executed. The third requirement captures that faults do not have to execute. Finally, the fourth requirement captures that the number of fault-occurrences in a computation is finite. This requirement is the same as that made in previous work \cite{dij, ak95, ag0, varghese-thesis} to ensure that eventually recovery can occur.
\noindent {\bf Fault-tolerance (F-tolerant)}. \ $\mathcal{A}$ is $F$-tolerant for specification $\mathit{spec}$ from $S$ iff the following two conditions hold: $(i) \mathcal{A}$ satisfies $\mathit{spec}$ from $S$, and $(ii)$ there exists $T$ such that $T$ is an $F$-span of $\mathcal{A}$ from $S$, and every computation of $\mathcal{A} [] F$ starting in a state where $T$ is true satisfies safety specification.
%there exists a fault-span $T$, such that starting from any state where $T$ is true, ($i$) safety specification is satisfied in any computation where actions of $\Sigma(\mathcal{P}) \cup \Sigma_a(\mathcal{P})$ are executed, and ($ii$) every computation of $\mathcal{P}$ alone eventually reaches a state where $S$ is true.
{\em Remark}. \ Henceforth, whenever the invariant $S$ and the program $\mathcal{A}$ are clear from the context, we will omit them; thus, ``$T$ is a $F$-span of $\mathcal{A}$ from $S$ for $\mathit{spec}$'' abbreviates to ``$T$ is a $F$-span''.
Let $F_P$ be the fault class of the old program (i.e., the program before adaptation) and $F_Q$ be the fault class of the new program (i.e., the program after adaptation). Let $S_P$ be an invariant and $T_P$ be a $F_P$-span of the old program. Similarly, let $S_Q$ be an invariant and $T_Q$ be a $F_Q$-span of the new program. The old program is $F_P$-tolerant, and the new program is $F_Q$-tolerant. Let $F$ be the fault class during adaptation.
%Hence, the program during adaptation can tolerate at most faults $F_P$. Similarly, the new program is $F_Q$-tolerant, and so the program can tolerate at most faults $F_Q$. We, therefore, define the fault class $F$ that we consider during adaptation as $F = F_P \cap F_Q$. We could as well have a subset of $F_P \cap F_Q$ as a fault class during adaptation.
In the context of adaptation, we define {\em transitional-faultspans} to identify the set of states that the program can reach while performing adaptation in presence of faults.
\noindent {\bf Transitional-faultspan}. \ Let $R$ be an intermediate program in the adaptation $\Delta$, and $\mathit{TS}$ be a transitional-invariant of $R$. A {\em transitional-faultspan} ($F$-span) of $R$ from $\mathit{TS}$ is a predicate $\mathit{TT}$ that satisfies following two conditions: $(i) \mathit{TS} \subseteq \mathit{TT}$, and $(ii) \mathit{TT}$ is closed in $R [] F$.
%Let $\mathit{TS}$ be a transitional-invariant predicate of an intermediate program, and let $F$ denote faults that are considered during adaptation. $\mathit{TT}$ is a {\em transitional-faultspan} ($F$-span) of the intermediate program from $\mathit{TS}$ iff $\mathit{TS} \Rightarrow \mathit{TT}$ and $\mathit{TT}$ is closed in $F$ and actions of the intermediate program. We note that program actions considered for closure of transitional-faultspans are actions of the old program that are not yet removed and actions of the new program that are already added.
Now, we define {\em transitional-faultspan lattice}.
\noindent {\bf Transitional-faultspan lattice}. \ A {\em transitional-faultspan ($F$-span) lattice} is an adaptation lattice where each node is associated with two predicates, a transitional-invariant and a transitional-faultspan, and the following conditions are satisfied:
\begin{enumerate}
\item[0.] {\bf Correctness in absence of faults}. \ The adaptation lattice obtained by considering the transitional-invariants only forms a transitional-invariant lattice.
\item[1.] {\bf Fault-tolerance of old program}. \ The entry node $P$ is associated with a $F_P$-span $T_P$ of the program before adaptation.
\item[2.] {\bf Fault-tolerance of new program}. \ The exit node $Q$ is associated with a $F_Q$-span $T_Q$ of the program after adaptation.
\item[3.] {\bf Fault-tolerance of intermediate program}. \ Each intermediate node $R$ is associated with a predicate $\mathit{TT}_R$ that is a transitional-faultspan ($F$-span) from $\mathit{TS}_R$ for any intermediate program at $R$ (i.e., intermediate program obtained by performing adaptations from the entry node to $R$). Furthermore, any intermediate program at $R$ is $F$-tolerant from $\mathit{TS}_R$.
% satisfies safety specification during adaptation from $\mathit{TT}_R$.
\item[4.] {\bf Safety of adaptive action}. \ If a node labeled $R_i$ has an outgoing edge labeled $a$ to a node labeled $R_j$, then for all adaptive transitions $(s, a, s^\prime)$ in $S_{\textit{map}}$ where $\mathit{TT}_{R_i}$ is true in state $s$, $\mathit{TT}_{R_j}$ is true in state $s^\prime$. Furthermore, all the adaptive transitions $(s, a, s^\prime)$ satisfies the safety specification during adaptation.
\item[5.] {\bf Progress of adaptation}. \ If a node labeled $R$ has outgoing edges labeled $a_1, a_2, ..., a_k$ to nodes $R_1, R_2, ..., R_k$, respectively, then in all computations of adaptation there exists a transition $(s, s^\prime)$ such that for some $i : 1 \leq i \leq k : (s, a_i, s^\prime) \in S_{\textit{map}}$. Furthermore, $\forall s: s \in \mathit{TT}_R : (\forall a, s^\prime: a \in \Sigma_a - \{a_1, ..., a_k\} : (s, a, s^\prime) \not\in S_{\textit{map}})$.
\end{enumerate}
\noindent {\bf Correctness of adaptation in presence of faults}. \ Intuitively, an adaptation is correct in presence of faults $F$ if the following conditions are satisfied: If the adaptation begins in a legitimate state of the old program then during adaptation each intermediate program is $F$-tolerant and the resulting state of the new program is legitimate. With this intuition, if adaptation begins in a state where fault-span of the old program is true, then we say that adaptation is correct if:
\begin{itemize}
\item Adaptation terminates in a state where fault-span of the new program is true
\item During adaptation, each intermediate program is $F$-tolerant
\item Eventually adaptation terminates
\end{itemize}
The following theorem states that finding a transitional-faultspan lattice is necessary and sufficient for proving correctness of adaptation.
\noindent {\bf Theorem 2}. \ {\it Given $S_P$ as the invariant of the program before adaptation, $T_P$ as the faultspan used to show that the program before adaptation is tolerant to $F_P$, $S_Q$ as the invariant of the program after adaptation, and $T_Q$ as the faultspan used to show that the program after adaptation is tolerant to $F_Q$, the adaptation from $P$ to $Q$ is correct in presence of faults $F$ if and only if there is a transitional-faultspan ($F$-span) lattice for the adaptation with start node associated with $S_P$ and $T_P$, and end node associated with $S_Q$ and $T_Q$.}
\vspace*{0.5mm}
\noindent {\em Proof}. The proof of this theorem is similar to the proof of Theorem $1$ discussed in Section \ref{til-sec}. \qed
%If there exists a transitional-faultspan lattice with entry node associated with $S_P$ and $T_P$, and exit node associated with $S_Q$ and $T_Q$, then the adaptation depicted by that lattice is correct in the presence of $F = F_P \cap F_Q$ (i.e., while the adaptation is being performed the specification and fault-tolerance requirements during adaptation are satisfied and after the adaptation completes, the application satisfies the new specification and fault-tolerance requirements)}. \qed
\noindent {\em Remark}. \ Different types of tolerance specifications that normally occur in practice, namely, {\em masking}, {\em fail-safe}, and {\em non-masking} tolerance have been considered in the previous work \cite{closure-arora, multitolerance, thesis-sandeep}. In above discussion, we have considered masking fault-tolerance. The definitions can be easily extended to consider the fail-safe and non-masking tolerance during adaptation.
\vspace*{-3mm}
\subsection{Adaptation of Self-Stabilizing Programs}
\vspace*{-3mm}
In this section, we consider the adaptation considered in \cite{adaptive-gouda} where the authors have focused on adapting from one self-stabilizing program into another self-stabilizing program \cite{dij}. We show that this is an instance of our approach where all the transitional-faultspan predicates are {\em true}.
A program is self-stabilizing if starting from an arbitrary state it eventually recovers to a legitimate state. Thus, in transforming from one stabilizing program to another, we can let all the fault-spans (i.e., fault-span of the old program, fault-span of the new program and transitional-faultspans of intermediate programs) be true. With this approach, if the old program starts in any state, eventually the new program execution begins although the state of the new program may be arbitrary. Since the new program is self-stabilizing, it will eventually recover to legitimate states.
Note that in \cite{adaptive-gouda} the corresponding transitional-invariants may not exist. Specifically, even if the old program begins in legitimate states, the new program may initially be in illegitimate states before recovery takes place. Moreover, \cite{adaptive-gouda} allows arbitrary behavior during adaptation and, hence, the specification during adaptation may not be met.
\iffalse
{\bf Self-stabilizing adaptation}. \ We consider a special case of adaptation where in the transitional-faultspan lattice corresponding to that adaptation, $\forall i: \mathit{TT}_{R_i} = \textit{true}$, and $T_Q = \textit{true}$. In this case, the adaptation starts in a correct state of the old program, may reach arbitrary states during adaptation and end in an arbitrary state, but after the adaptation completes, eventually the new program will reach a state from where it will satisfy its new specification. The new program is a {\em self-stabilizing} (\cite{dij}) program and we define this type of adaptation as {\em self-stabilizing adaptation}.
Informally, a self-stabilizing program is defined as a distributed computer program that returns to a legitimate state from any arbitrary state in a finite amount of time without any external (e.g. human) intervention.
This notion of self-stabilizing adaptation is similar to the notion used in \cite{adaptive-gouda}, where the old and new program are self-stabilizing and upon replacement of components the resulting program eventually reaches its legitimate state.
%\begin{theorem} Given $S_P$ as an invariant, $T$ as a $F$-span, and $T_P$ as a $F_P$-span of the program before adaptation and $S_Q$ as an invariant, $T^{\prime}$ as a $F$-span, and $T_Q$ as a $F_Q$-span of the program after adaptation, if there exists a transitional-faultspan lattice with entry node associated with $S_P$ and $T$, and exit node associated with $S_Q$ and $T^{\prime}$, then the adaptation depicted by that lattice is correct in presence of $F = F_P \cap F_Q$ (i.e., while the adaptation is being performed the specification and fault-tolerance requirements during adaptation are satisfied and after the adaptation completes, the application satisfies the new specification and fault-tolerance requirements). \qed \end{theorem}
\fi