## 3 Approach
### Probabilistic Validation  
The verification of all the SSReqs (safety and security requirements) of a system is performed by the SSReq verifier for all probabilistic execution paths of the probabilistic execution model. The total probability of satisfying the requirements is obtained by summing all the probabilities of the paths where the requirements are satisfied. For example, Table 7 shows the results of the probabilistic verification of all the SSReqs of System \(P_{1}^{\prime}B_{1}^{\prime}C_{1}^{\prime}\) listed in Table 6. The satisfaction probabilities for the requirements are 0.18, 0.27, 0.18 and 0.09, respectively, and were obtained as follows. Note that \(P_{r}\) and \(P_{e}\) represent the probabilities for requirements and execution, respectively. * \(p_{r}\big{(}R_{1}^{sc}\big{)}=p_{e}(ePath_{1})+p_{e}(ePath_{10})=0.168+0.012=0.18\);
* \(p_{r}(R_{2}^{sc})=p_{e}(ePath_{1})+p_{e}(ePath_{4})+p_{e}(ePath_{7})+p_{e}(ePath _{10})=0.168+0.168+0.048+0.012=0.27\);
* \(p_{r}\big{(}R_{1}^{sf}\big{)}=p_{e}(ePath_{1})+p_{e}(ePath_{10})=0.168+0.012=0.18\); \begin{table}
\begin{tabular}{c c c c} \hline \multicolumn{2}{c}{**SSReq**} & **VaReg** & **Validation** \\ \hline \multirow{6}{*}{\(R_{1}^{ss}\)} & & The order of the resources, that is, \(R1\)–\(R2\) or & \\  & & \(R2\)–\(R1\), should not be violated because the & \\  & \(R_{1}^{sc}\) & security information is contained in the first & \\  & & resource (\(R1\)) to decode the second resource & \\  & & (\(R2\)) or vice versa. & \\ \cline{2-4}  & \(R_{2}^{sc}\) & The propagation between the first (\(R1\)) and & \\  & & second (\(R2\)), or vice versa, should not be more & \\  & & than 3 time units. & \\ \hline \multirow{6}{*}{\(R_{2}^{ss}\)} & & The deadline for the consumption of the second & \\  & \(R_{1}^{sf}\) & resource (\(R2\)) by \(C_{1}^{\prime}\) should not be more than & \\  & & 10 time units for the order of the resources & \\ \cline{1-1}  & & \(R1\)–\(R2\). & \\ \cline{1-1} \cline{2-4}  & & The deadline for consumption of the second & \\ \cline{1-1}  & \(R_{2}^{sf}\) & resource (\(R2\)) by \(C_{1}^{\prime}\) should not be more than & \\ \cline{1-1}  & & 11 time units for the order of the resources & \\ \cline{1-1}  & & \(R2\)–\(R1\). & \\ \hline \end{tabular}
\end{table} 
Table 6: SSReqs for the PBC (Producer–Buffer–Consumer) example. Figure 3: Conceptual probabilistic EX (execution) model. Note that \(R_{1}^{sc}\) is a subset of \(R_{2}^{sc}\), and \(R_{2}^{sf}\) and \(R_{2}^{sf}\) are disjointed, meaning that there is no dependency among the requirements. However, it is necessary to analyze the dependencies among the requirements in order to prevent some contradictions and discrepancies from being specified during the verification process. The validation requirement for a safety and security requirement is defined by the probability that the requirement is satisfied in the probabilistic execution model of the target system. For example, the left side of Table 8 shows the validation requirements for all the safety and security requirements of System \(P_{1}^{\prime}B_{1}^{\prime}C_{1}^{\prime}\): 0.10, 0.15, 0.10, and 0.05 for \(R_{1}^{sc}\), \(R_{2}^{sc}\), \(R_{1}^{sf}\), and \(R_{2}^{sf}\), respectively. The validation of each probabilistic safety and security requirement is performed by comparing the probability for the validation requirement with the probability for the satisfaction of the requirement in the probabilistic execution model of the target system. If the former is less than the latter, the validation requirement is _satisfied_. If not, it is _unsatisfied_. For example, the validation requirements for all the safety and security requirements of System \(P_{1}^{\prime}B_{1}^{\prime}C_{1}^{\prime}\) are satisfied, as shown in Table 8. However, if the validation requirements are tightened, as shown in the left side of Table 9, some requirements become _unsatisfied_ for their validation: \(R_{1}^{sc}\) and \(R_{1}^{sf}\).