# System-Theoretic Process Analysis Based on SysML/MARTE and NuSMV
## 2 STPA-SN  
STPA-SN consists of four steps, as shown in Figure 1. Each step is briefly introduced as follows:  
1. Step 1: Define the purpose of the analysis. The contents of STPA-SN in this step are basically the same as those in the first step of HSTPA, but the definition of \"system-level hazard\" is optimized. HSTPA defines system-level hazards as follows: \"A hazard is a system state or set of conditions that, together with a particular set of worst-case environmental conditions, will lead to a loss\". Since a hazard does not necessarily occur under \"worst environmental conditions\", STPA-SN slightly changes the definition as \"System-level hazard is a system state that can lead to a loss under certain conditions\" and loss scenario provides such conditions. Among the outputs of Step 1, the safety constraints (SCs) will be used in Step 4 to create safety properties in temporal logic, i.e., computation tree logic (CTL) or linear temporal logic (LTL) (see NuSMV tutorial in [13]). 2. Step 2: Construct the system model. This step constructs the analytical model for the identifications of UCAs and loss scenarios. SysML internal block diagram (IBD) is used to construct the hierarchical control structure model, and the SysML state machine diagram is used to describe the system behaviors. The system behaviors required to identify UCAs and identify loss scenarios are all described by SysML state machine diagrams, including the behaviors of the controller, controlled process, sensor, actuator and their interaction relationships, therein controller behaviors further include the process model and control algorithms. Due to time-dependent UCAs, the modeling methods need to describe the temporal characteristics. Since MARTE and SysML are closely interrelated, MARTE is used to describe the temporal characteristics. 3. Step 3: Identify the unsafe control actions. The system-level hazard is caused by the state of the controlled process and CA-PR. CA-PR is different from the control action issued by the controller because of the actuator's delay or mishandling. Hence, CA-PR is used in the definition of UCA, instead of the control action issued by the controller. In STPA-SN, UCA is such a combination as {CA-PR, Type, Context}, which leads to system-level hazards under certain conditions. Therein, Type stands for unsafe type and Context is the state of the system, controlled process and the environment. When identifying UCAs, all instances of {CA-PR, Type, Context} should be given first, with each instance considered as a potential unsafe control action (PUCA). This process could be automated. Then, each PUCA is analyzed one by one to determine whether it is a UCA. This process relies heavily on manual analysis, though truth calculation could play a role. Figure 1: Steps of STPA-SN. Step 4: Identify the loss scenarios. STPA-SN adopts the definition of loss scenario as the process in which the system emerges UCA and system-level hazard with the involvement of causal factors. There are many causes, such as hardware failure, software defect, data deviation, data error, process model error, component interaction, mode change, environmental change, environmental interference, controlled process change, feedback missing or error, feedback delay, actuator failure or delay, etc. There are two ways to analyze the models constructed in Step 2: one is simulation, the other is model checking. Simulation is usually visualized, but could not exhaust all the operations of the system model. Hence, theoretically, simulation may miss loss scenario, which may be unaccepted for the safety-critical system. Model checking is a formal method, requiring more expertise. However, model checking can prove whether the system model meets some safety attributes or properties, which is precious to the safety-critical system. Since STPA highlights the high-level design logics of the system, and control actions are usually discrete logical variables, model checking is selected to identify the loss scenario.