# SDN-Based Survivability Analysis for V2I Communications
## 5 Verification and Analysis of V2I Networks Survivability Model
### Analysis of Maximum Survival Probability of V2I Networks  
To further analyze the survivability model, we define the relevant CSL [39; 40] property formulas through the property syntax and semantic rules of the probabilistic model checker to study the survivability model from multiple angles. In PRISM, the probability calculation in the definition CSL probability property formula is carried out by the operation P, which has the following form:  
\[P=?[\textit{pathprop}], \tag{20}\]  
where \"\(P\)\" represents the probabilistic results, the symbol \"?\" denotes the probability calculation, and \"_pathprop_\" indicates the path property. By this way, the maximum survival probability of the V2I network is analyzed on the basis of the time boundary. The property formula is defined by CSL as follows:  
\[P_{\textit{sur\_max}}=?[\textit{trueU}<=T(n=N)\&(j=3*N)\{(n<N)\&(j<3*N)\}|\{ \max\}]. \tag{21}\]  
The formula indicates the maximum survival probability of the V2I network within the time boundary \(T=20\), when the state \((n,j)\) reaches the target state from the initial state. From Equation (20), we can analyze the survivability of the V2I network from the angle of the influence of different parameters in the survivability model. To distinguish the survival probability under each condition, the experimental simulation is represented by \(P_{\textit{sur\_max1}}\), \(P_{\textit{sur\_max2}}\), \(P_{\textit{sur\_max3}}\) and \(P_{\textit{sur\_max4}}\), respectively. In Figure 6, we discuss the variation of the survival probability of V2I network with time. To facilitate analysis, the number \(N\) of vehicles in the diagram is 10, the V2I link failure rate \(\lambda_{1}\) and vehicle node failure rate \(\lambda_{2}\) are both considered as a fixed value. It is observed that the survival probability \(P_{\textit{sur\_max1}}\) of the V2I network also increases as the corresponding repair rate \(\mu_{1}\) and \(\mu_{2}\) increase from 0.1 to 0.9, respectively. When both repair rates are small (e.g., \(\mu_{1}\) and \(\mu_{2}\) are 0.1, 0.2), the survival probability \(P_{\textit{sur\_max1}}\) of the V2I network is low. The survival probability \(P_{\textit{sur\_max1}}\) does not greatly change in 5 s, and basically remained at the stable value, and after the repair rate of both increased to 0.5, the survival probability \(P_{\textit{sur\_max1}}\) with the change of time also increased rapidly. After a certain period of time, the survival probability \(P_{\textit{sur\_max1}}\) of the V2I network achieves maximum value 1. The results show that the reachability of each state in the survivability model satisfies the requirements of defining properties and achieves the maximum survival probability. \begin{table}
\begin{tabular}{c c c c c c c c} \hline \hline \multirow{2}{*}{**Vehicle**} & \multicolumn{2}{c}{**Model**} & \multicolumn{2}{c}{**MTBDD**} & \multicolumn{2}{c}{**Costruction**} & \multicolumn{2}{c}{**Reachability**} \\  & & & & & & & **Time(s)** & **Iter. (s)** \\ \hline
10 & 341 & 1451 & 456 & 31 & 0.017 & 41 & 0.00024 \\
50 & 7701 & 37,251 & 2877 & 151 & 0.04 & 201 & 0.000104 \\
100 & 30,401 & 1  
In what following, we discuss the survival probability \(P_{sur\_max2}\) of the V2I vehicle network with the number of vehicle failures. Since the number of failures that exist in different vehicle nodes is considered, the failure of the vehicle node will indirectly lead to an interruption from the corresponding V2I network communication link of vehicles. Therefore, we analyze the survival probability \(P_{sur\_max2}\) of V2I network under different vehicle failure numbers \(n\), the specific situations are shown in Figure 7. We set \(\lambda_{1}=\lambda_{2}=0.1\), the number of vehicles is \(N=50\), and the number of vehicle failures \(n\leq N\). The survival probability \(P_{sur\_max2}\) of the V2I network under different vehicle node repair rate \(\mu_{2}\) is compared in the Figure 7. The results show that the survivability probability \(P_{sur\_max2}\) of V2I network decreases with the increase of failures.