# System-Theoretic Process Analysis Based on SysML/MARTE and NuSMV
###### Abstract  
Systems Theoretical Accident Model and Process (STAMP), which considers system safety as an emergent property of the system, is a more effective accident/loss causality model for modern complex systems. Based on STAMP, System Theoretical Process Analysis (STPA) has attracted increasing attention as a new approach to hazard analysis, and relevant international standards are being developed. However, STPA is mainly performed manually, leading to inefficiencies, and constructs models in non-standard language, hindering the integration with existing systems engineering. STPA-SN (STPA based on SysML/MARTE and NuSMV) is proposed to build model in SysML, describing the timing with MARTE (Modeling and Analysis of Real-Time and Embedded Systems), transform SysML model into NuSMV model and output loss scenarios automatically with model checker. An application example of STPA-SN is provided to demonstrate potentials for higher efficiency of analysis and for collaboration with SysML-based systems engineering. system theory process analysis (STPA); SysML; NuSMV; unsafe control action (UCA); loss scenario +
Footnote †: journal: Applied  
Step 2: Model the control structure. An effective control structure will enforce constraints on the behavior of the overall system. The hierarchical control structure model includes at least five types of elements: controllers, controlled processes, control actions, feedbacks and inputs/outputs among other components. The controller includes control algorithms and the process model. Step 3: Identify the unsafe control actions. An unsafe control action (UCA) is a control action that will lead to a hazard in a particular context and worst-case environment. The UCA consists of five parts: control action (CA), source of CA, unsafe type, context and link to hazards. The unsafe types include:  
* Provided CA;
* Provided CA too early or provided CA too late;
* Stopped CA too early or applied CA too long. Step 4: Identify the loss scenarios. The loss scenario describes the causal factors (CFs) that can lead to UCAs and to hazards. At present, HSTPA still has two drawbacks in industrial practice:  
* Manual analysis, which is inefficient [2] (p. 151);
* Modeling with non-standard language, which is difficult to be integrated into existing systems engineering. Automation can improve the efficiency, and the formalization of STPA is the basis for automation. Only after formalizing STPA can tools be developed to realize automation and may STPA support standardized modeling languages, such as SysML, AADL and AltaRica. The formalization of STPA includes the definitions of UCA and loss scenario, the construction of the analytical model, the identification processes of UCAs and the loss scenarios. The related representative work is described below. [PERSON] [3] formalized the definition of UCA, which was adopted by HSTPA. However, there are still some ambiguities. It is not specified whether UCA is a state or not. Similarly, it is not specified whether the CA in the definition of UCA is the one received by the controlled process or the one issued by the controller, which may lead to critical differences while identifying the loss scenario. [PERSON] [3] identified UCAs with truth calculations, which was adopted by many subsequent works, e.g., [4; 5]. Under certain conditions, the truth calculation is effective to identify UCAs automatically. [PERSON] et al. [2] and [PERSON] et al. [6] proposed their respective formal analysis methods, which include analytical model construction and model analysis. They suffer from shortcomings in terms of ease of use and quality of analysis due to the inability to use existing established methods. Although STPA has the concepts of UCA and the loss scenario, the STPA analytical model is still able to be modeled with existing mature model methods, such as SysML and AADL. Similarly, the STPA analytical model can be analyzed by existing mature analytical methods, such as model checking and simulation. [PERSON] et al.