## 4 Implementation
### Smart EMS System
#### 4.3.1 Description
\(TRANSFER\_to\_HospM_{1}(\overline{T2})\{0.1\}\)--the probability that \(\text{AmbX}_{1}\) transmits the information of a T2 patient at LocB to \(\text{HospM}_{1}\) (10%). 8. \(\text{AmbY}_{1}\) receives the patient's information from 911 Center\({}_{1}\) and transfers the patient to \(\text{HospN}_{1}\) after rescuing the patient; 1. \(ORDER\_AmbY_{1}(T2-T3)\{0.7\}\)--the probability that \(\text{AmbY}_{1}\) moves first to LocC (70%); 2. \(ORDER\_AmbY_{1}(T3-T2)\{0.3\}\)--the probability that \(\text{AmbY}_{1}\) moves first to LocD (30%); 3. \(TRANSFER\_to\_HospN_{1}(\overline{T2})\{0.9\}\)--the probability that \(\text{AmbY}_{1}\) transmits the information of a T2 patient at LocC to \(\text{HospN}_{1}\) (90%); 4. \(TRANSFER\_to\_HospN_{1}(\overline{T3})\{0.1\}\)--the probability that \(\text{AmbY}_{1}\) transmits the information of a T3 patient at LocD to \(\text{HospN}_{1}\) (10%). 9. \(\text{HospM}_{1}\) receives the patient from \(\text{AmbX}_{1}\); 1. \(TRANSFER\_to\_HospM_{1}(T1)\{0.9\}\)--the probability that \(\text{HospM}_{1}\) receives the information on a T1 patient at LocA (90%); 2. \(TRANSFER\_to\_HospM_{1}(T2)\{0.1\}\)--the probability that \(\text{HospM}_{1}\) receives the information on a T2 patient at LocB (10%). 10. \(\text{HospN}_{1}\) receives the patient from \(\text{AmbY}_{1}\). 1. \(TRANSFER\_to\_HospN_{1}(T2)\{0.9\}\)--the probability that \(\text{HospN}_{1}\) receives the information on a T2 patient at LocC (90%); 2. \(TRANSFER\_to\_HospN_{1}(T3)\{0.1\}\)--the probability that \(\text{HospN}_{1}\) receives the information on a T3 patient at LocD (10%). 11. \(\text{HospN}_{1}\) receives the patient from \(\text{AmbY}_{1}\). 1. \(\text{HospN}_{1}\) receives the patient from  
Figure 8 and 9 show the ITL (In-The-Large) model and the ITS (In-The-Small) models in SAVE (Specification, Analysis, Verification, Evaluation) for the dTP-Calculus code in Figure 7.  
Figure 8: ITL model in SAVE for the smart EMS example (detailed view in Appendix A). Figure 7: The smart EMS example in dTP-Calculus. Figure 11: Conceptual representation of the step-wise accumulative probabilities for the smart EMS example (detailed view in Appendix A). \begin{table}
\begin{tabular}{l c c c} \hline \hline
**Path** & **Probability** & **Path** & **Probability** \\ \hline
1 & 0.260514 & 24 (Deadlock) & 0.090095 \\ \hline
2 (Deadlock) & 0.028985 & 25 & 0.003193 \\ \hline
3 (Deadlock) & 0.028968 & 26 (Deadlock) & 0.000362 \\ \hline
4 & 0.003227 & 27 (Deadlock) & 0.000355 \\ \hline
5 (Deadlock) & 0.137511 & 28 & 0.000042 \\ \hline
6 (Deadlock) & 0.137929 & 29 (Deadlock) & 0.001706 \\ \hline
7 & 0.047687 & 30 (Deadlock) & 0.001679 \\ \hline
8 (Deadlock) & 0.005240 & 31 & 0.000601 \\ \hline
9 (Deadlock) & 0.005317 & 32 (Deadlock) & 0.000071 \\ \hline
10 & 0.000629 & 33 (Deadlock) & 0.000073 \\ \hline
11 (Deadlock) & 0.072801 & 34 & 0.000008 \\ \hline
12 (Deadlock) & 0.073120 & 35 (Deadlock) & 0.000840 \\ \hline
13 & 0.003201 & 36 (Deadlock) & 0.000924 \\ \hline
14 (Deadlock) & 0.000347 & 37 & 0.000037 \\ \hline
15 (Deadlock) & 0.000358 & 38 (Deadlock) & 0.000005 \\ \hline
16 & 0.000034 & 39 (Deadlock) & 0.000005 \\ \hline
17 (Deadlock) & 0.001706 & 40 & 0.000002 \\ \hline
18 (Deadlock) & 0.001695 & 41 (Deadlock) & 0.000021 \\ \hline
19 & 0.000589 & 42 (Deadlock) & 0.000019 \\ \hline
20 (Deadlock) & 0.000062 & 43 & 0.000008 \\ \hline
21 (Deadlock) & 0.000065 & 44 (Deadlock) & 0.000001 \\ \hline
22 & 0.000005 & 45 (Deadlock) & 0.000002 \\ \hline
23 (Deadlock) & 0.089958 & 46 & 0.000003 \\ \hline \hline \end{tabular}
\end{table} 
Table 13: Path probabilities for the smart EMS example using SAVE. As shown in Figure 13 and Table 16, the present system cannot satisfy all the probabilistic safety and security requirements for the example. Note that the capabilities of the IoT for each version can be determined by those of the IoT devices with the probabilities, as shown in Tables 12 and 13 in Appendix A.