# System-Theoretic Process Analysis Based on SysML/MARTE and NuSMV
## 3 STPA-SN Application Example
### Step 3: Identify the Unsafe Control Actions
#### 3.3.4 Analyze Each PUCA to Determine Whether It Is a UCA  
Analyze PUCAs one by one. Similar to [3; 4; 5], truth calculations could be used. A PUCA is a UCA if it implies that the expression of H1 in Section 3.3.1 is true.  
By truth calculation, the PUCA of ID 9 is judged as true UCA, but equal to H1, because the PUCA of ID 9 means CA-PR= Act_Close_CA, Type = Provided, PhysicalDoor = physicalOpened and PhysicalObstacle = physicalExisting.  
However, for those PUCAs that could not be judged as true UCAs by truth calculations, they still need to be analyzed manually, since truth calculations only apply to those PUCAs, which are the instances of hazards already identified in Step 1 of STPA-SN. This means the manual identification of UCA is indispensable. Hence, the remaining 63 PUCAs should be analyzed manually.  
Since Act_Open_CA and Act_Close_CA are discrete commands and not continuous ones, Type 4 is not applicable. Assuming PhysicalClosed and PhysicalExisting cannot be true simultaneously, the corresponding entries are also not applicable.  
Through manual analysis, many of the PUCAs are judged as true UCAs, each of which causes a new hazard to be identified.  
\begin{table}
\begin{tabular}{c|c|c|c|c|c} \hline \hline \multicolumn{2}{c}{**PUCAs**} & \multicolumn{2}{c}{**Analysis Results of PUCAs**} \\ \hline \multirow{2}{*}{**ID**} & \multirow{2}{*}{**CA-PR**} & \multirow{2}{*}{**Type**} & \multicolumn{2}{c|}{**Context**} & \multirow{2}{*}{**Analysis**} & \multirow{2}{*}{**A True UCA or Not**} \\ \cline{3-3} \cline{5-5}  & & & **PhysicalDoor** & **PhysicalObstacle** & & **Method** \\ \hline
25 & & & & & Manual \\ \hline
26 & & & & & Manual \\ \hline
27 & & & & & Manual \\ \hline
28 & & & & & Manual \\ \hline
29 & & & & Manual \\ \hline
30 & & & & Manual \\ \hline
31 & & & & Manual \\ \hline
32 & & & & Manual \\ \hline \(\ldots\) & & & Manual & \\ \hline \(\ldots\) & & & Manual & \\ \hline \(\ldots\) & & & Manual & \\ \hline \(\ldots\) & & & Manual & \\ \hline
49 & & & & Manual \\ \hline
50 & & & PhysicalCoEristing & Manual & \\ \hline
51 & & & PhysicalCoEristing & Manual & \\ \hline
52 & & & PhysicalCoEristing & Manual & \\ \hline
53 & Act\_Open\_CA & Type 3 & PhysicalOpening & PhysicalExisting & Manual & \\ \hline
54 & & & & Manual \\ \hline
55 & & & PhysicalCoEristing & Manual & \\ \hline
56 & & & PhysicalCoEristing & Manual & \\ \hline \(\ldots\) & & & Manual & \\ \hline
64 & & & Manual & \\ \hline \hline \end{tabular}
\end{table}
Table 3: _Cont._For example, the PUCA with ID 55 means that door receives CA-PR = Act_Open_CA with Type 3 when PhysicalDoor = PhysicalClosing and PhysicalObstacle = PhysicalExisting. This PUCA would be a hazard if receiving CA-PR = Act_Open_CA too late; therefore, this PUCA is a true UCA and a new hazard can be generated, marked as H2. By design, the meaning of \"too late\" is defined as \"later more than 3 units of time\".  
Although every true UCA, which is judged by manual analysis, causes a new hazard to be identified, it does not mean every true UCA will correspond to a new hazard one-to-one; instead, several true UCAs could correspond to a common new hazard.  
After the new hazards are identified, the system-level hazards will be updated. Here, the system-level hazards are updated as follows after H2 is added:  
* H1: PhysicalDoor = physicalOpened and PhysicalObstacle = physicalExisting and Act_Close_CA = TRUE.
* H2: PhysicalDoor = physicalClosing and PhysicalObstacle = physicalExisting and (the time, from Obs_Existing to Act_Open_CA when physicalClosing = TRUE, is larger than 3 units of time).  
Corresponding to the hazards H1 and H2, the safety constraints of the system are determined as follows:  
* SC1: PhysicalDoor = physicalOpened, PhysicalObstacle = physicalExisting, Act_Close_CA = TRUE, these three conditions cannot hold simultaneously.
* SC2: PhysicalDoor = physicalClosing, PhysicalObstacle = physicalExisting, (the time, from Obs_Existing to Act_Open_CA when physicalClosing = TRUE, is larger than 3 units of time), these three conditions cannot hold simultaneously.