## 4 Implementation
### Smart EMS: Incremental System Improvement
#### 4.4.1 Incremental System Improvement by Single Process Enhancement  
Figure 14 shows the improvement of AmbX from AmbX\({}_{1}\) to AmbX\({}_{4}\) with the enhanced probabilities, as follows:  
1. The probabilities that 911 Center\({}_{1}\) sends AmbX\({}_{1}\) the rescue order for the patients are updated where \(\bullet\)\(ORDER\_Ambx_{1}\big{(}\overline{T1-T2}\big{)}\{0.99\}\)--the probability that a T1 patient at LocA is rescued first (99%); \begin{table}
\begin{tabular}{c c c c c c} \hline \multicolumn{2}{c}{**Requirements**} & \multicolumn{2}{c}{**Va Probabilities**} & \multicolumn{2}{c}{**System Probabilities**} & \multicolumn{2}{c}{**Verification Results**} \\ \hline \multirow{4}{*}{\(R^{Sc}\)} & \(R^{Sc}_{1}\) & 0.35 & 0.32 & X & \begin{tabular}{c} Unsatisfied, \\ but Satisfiable \\ \end{tabular} \\ \cline{2-6}  & \(R^{Sc}_{2}\) & 0.40 & 0.32 & X & \begin{tabular}{c} Unsatisfied, \\ but Satisfiable \\ \end{tabular} \\ \cline{2-6}  & \(R^{Sc}_{3}\) & 0.30 & 0.27 & X & \
\begin{tabular}{c} Unsatisfied, \\ but Satisfiable \\ \end{tabular} \\ \hline \multirow{4}{*}{\(R^{Sf}\)} & \(R^{Sf}_{1}\) & 0.50 & 0.31 & X &
\begin{tabular}{c} Unsatisfied, \\ but Satisfiable \\ \end{tabular} \\ \cline{2-6}  & \(R^{Sf}_{2}\) & 0.30 & 0.32 & O & Satisfied \\ \cline{1-1} \cline{2-6}  & \(R^{Sf}_{3}\) & 0.20 & 0.32 & O & Satisfied \\ \hline \end{tabular}
\end{table} 
Table 16: Analysis of the validation of the probabilistic requirements for the smart EMS example. Figure 13: Analysis of the validation of the probabilistic requirements for the smart EMS example. \(ORDER\_AmbX_{1}\big{(}\overline{T2-T1}\big{)}\{0.01\}\)--the probability that a T2 patient at LocB is rescued first (1%). 2. \(\text{AmbX}_{1}\) receives the patient's information from 911 Center\({}_{1}\), and transfers the patient to \(\text{HospM}_{1}\) after rescuing the patient, with the updated probabilities. \(ORDER\_AmbX_{1}(T1-T2)\{0.99\}\)--the probability that \(\text{AmbX}_{1}\) moves first to LocA (99%); \(ORDER\_AmbX_{1}(T2-T1)\{0.01\}\)--the probability that \(\text{AmbX}_{1}\) moves first to LocB (1%). Figure 15 shows the EX model for the smart EMS system S\({}_{1}\) (HospM\({}_{1}\), \(\text{AmbX}_{1}\), \(911\text{Center}_{1}\), \(\text{AmbY}_{1}\), \(\text{HospN}_{1}\)) and the EX Model for the smart EMS system S\({}_{2}\) (HospM\({}_{1}\), \(\text{AmbX}_{4}\), \(911\text{Center}_{1}\), \(\text{AmbY}_{1}\), \(\text{HospN}_{1}\)) improved by the enhancement of \(\text{AmbX}_{1}\) to \(\text{AmbX}_{4}\). \begin{table}
\begin{tabular}{c c} \hline \hline
The figure shows that the two EX models are identical in shape, but it is not clear whether they are probabilistically equivalent or not within the permissible range of probabilities. In order to demonstrate probabilistic system equivalence between \(S_{1}\) and \(S_{2}\), Tables 18 and 19 are constructed to represent the probabilities for the all the system transitions represented in the EX model for \(S_{1}\) and EX model for \(S_{2}\), respectively. As shown in Tables 18 and 19, all the probabilities in Table 18 are within the range of those in Table 19, that is, (\(\Delta^{\langle(0.0),(0.09,0.09),\langle 0.0,0.0\rangle,(0.0,0.0),\langle 0,0.0\rangle,\langle 0.0\rangle\rangle}\)). It implies that two systems are probabilistically equivalent within the (\(\Delta^{\langle(0.0),(0.09,0.09),(0.0.0,0.0),\langle 0.0,0.0\rangle,\langle 0,0.0\rangle\rangle}\)) permissible range as follows:  
\[\textit{Smart}\;\textit{EMS}\;\textit{System}\;S_{1}^{\Delta^{\langle(0.0),(0.09,0.09),(0.0,0.0),(0.0,0.0),(0.0)\rangle}}\approx\textit{Smart}\;\textit{EMS}\; \textit{System}\;S_{2}\]  
Table 20 shows the validation results for probabilistic verification by the incremental improvement for Ambulance X from AmbX\({}_{1}\) to AmbX\({}_{4}\). The table shows that AmbX\({}_{4}\) satisfies two more probabilistic requirements, that is, \(R_{3}^{Sc}\) and \(R_{1}^{Sf}\), than the previous system with the old version AmbX\({}_{1}\).