# System-Theoretic Process Analysis Based on SysML/MARTE and NuSMV
## 3 STPA-SN Application Example
### Step 2: Construct the System Model
#### 3.2.2. Construct the System State Machine Diagrams  
STPA-SN uses MARTE to define clocks, including the two clocks as shown in Figure 3. These clocks are used to describe the time properties of the states and transitions. Their detailed purposes are shown in Table 2. \begin{table}
\begin{tabular}{c c} \hline \hline
**Commands or Feedbacks** & **Meaning** \\ \hline Drv\_Open\_CA & Open and close commands sent by the Driver, passed to \\ Drv\_Close\_CA & the DoorController \\ \hline Ctlr\_Open\_CA & Open and close commands sent by the DoorController, \\ Ctlr\_Close\_CA & passed to the DoorActuator \\ \hline Act\_Open\_CA & Open and close commands sent by the DoorActuator, \\ Act\_Close\_CA & passed to the PhysicalDoor \\ \hline Dr\_Closed & The states of the PhysicalDoor, which, respectively, \\ Dr\_Closing & represent “completely closed”, “in the process of closing”, \\ Dr\_Opened & “completely opened” and “in the process of opening” \\ Dr\_Opening & \\ \hline DrSrn\_Closed\_FB & The feedbacks provided by the DoorSensor to the \\ DrSmr\_Closing\_FB & DoorController. They indicate the door states sensed by \\ DrSmr\_Opened\_FB & the DoorSensor, which are “completely closed”, “in the \\ DrSmr\_Opening\_FB & process of closing”, “completely opened” and “in the \\  & process of opening”, respectively \\ \hline ObsSnr\_Existing\_FB & The feedback from the ObstacleSensor feedbacks to the \\ ObsSnr\_NotExisting\_FB & DoorController indicating whether the ObstacleSensor has \\  & sensed an obstacle in the doorway or not \\ \hline Obs\_Existing & Indicate whether there is an obstacle in the doorway \\ Obs\_NotExisting & \\ \hline \hline \end{tabular}
\end{table} 
Table 1: The meaning of each command or feedback. Figure 2: Internal block diagram of the train door control system. Corresponding to 7 parts in Figure 2, the system has 7 state machines, as shown in Figure 4. Every state machine corresponds to a state variable. They are, respectively, the Driver, DoorController, DoorActuator, DoorSensor, PhysicalDoor, ObstacleSensor and PhysicalObstacle. 1. Driver state machine. As Figure 4a shows, the driver can send Drv_Open_CA to the door controller and changes from driverOutputClose to driverOutputOpen. Similarly, the driver can send out Drv_Close_CA and changes from driverOutputOpen to driverOutputClose. 2. DoorController state machine. As Figure 4b shows, when Drv_Open_CA is true, the door controller sends Cltr_Open_CA. When the obstacle sensor finds an obstacle in the doorway (i.e., Obsnr_Existing_FB is true), the door controller will send Cltr_Open_CA to open the door. When DoorController is in the state of controllerOutputOpenCommand, if the obstacle sensor finds an obstacle in the doorway (i.e., Obsnr_Existing_FB is true), the door controller will send Cltr_Open_CA to open the door. The absence of obstacle (i.e., Obsnr_NotExisting_FB is true) is a necessary condition for the door controller to send Cltr_Close_CA. When the door is in the opening process (i.e., DoorSensor = sensedOpening), the controller will not send Cltr_Close_CA. \begin{table}
\begin{tabular}{c c} \hline \hline
**Clock Name** & **Purpose** \\ \hline clkDoorOpeningDuration & Records the time taken for the door to open, starting if Dr\_Opening is true and ending if Dr\_Opened is true \\ \hline clkDoorClosingDuration & Records the time taken for the door to close, starting if Dr\_Closing is true and ending if Dr\_Closed is true \\ \hline \hline \end{tabular}
\end{table} 
Table 2: The needed clocks and their purposes. Figure 3: Defining clocks with MARTE. Figure 4: _Cont_. 3. DoorActuator state machine. As Figure 4c shows, the actuator sends Act_Open_CA when receives Ctrlr_Open_CA and sends Act_Close_CA when receives Ctrlr_Close_CA. 4. DoorSensor state machine. As Figure 4d shows, the door sensor will feed back the corresponding information to the train door controller according to the actual status of the door. 5. PhysicalDoor state machine.