STPA method and device for accurate identification of loss scenarios
The present invention provides an STPA method and apparatus for accurate identification of a loss scenario. The method comprises: defining the purpose of the analysis, comprising identifying of a loss; modeling a system state machine using a finite state machine; identifying an unsafe control action using the identified loss and the modeled system state machine. The method according to the present invention achieves accurate and efficient identification of loss scenarios of a complex system using state machines and model checking techniques.
1. A System-Theoretic Process Analysis (STPA) method for automatically identifying a loss scenario in a system composed of hardware and/or software components, the method being implemented by a processor and comprising:
defining a purpose of analysis, comprising identifying a loss associated with the system;
modeling a system state machine using a finite state machine, the modeling being performed (i) with or without incorporating additional causal factors, and (ii) with or without modeling any faulty component;
identifying an unsafe control action using the loss associated with the system and the modeled system state machine, wherein identifying an unsafe control action using the loss associated with the system and the modeled system state machine comprises:
generating a Potential Unsafe Control Action (PUCA), said PUCA comprising:
a control action received by the controlled process;
a type; and
a context, wherein the type comprises:
a time-independent type, which comprises not providing a control action or providing a control action; or
a time-dependent type, which comprises providing a control action too early, too late, in a wrong order, lasting too long, or ending too quickly;
determining whether the PUCA is the unsafe control action based on the loss associated with the system and the generated PUCA, wherein the unsafe control action constitutes a system-level hazard, and wherein the unsafe control action having the time-independent type is referred to as a time-independent unsafe control action, and the unsafe control action having the time-dependent type is referred to as a time-dependent unsafe control action;
identifying the loss scenario using a model checking technique and the identified unsafe control action, wherein the model checking is an automated verification technique that comprises a model to be checked, a property to be checked, and a model checking algorithm,
and wherein identifying the loss scenario using the model checking technique and the identified unsafe control action comprises:
forming, based on the unsafe control action, a property to be checked using a model checking logic language, wherein, if the unsafe control action is a time-dependent unsafe control action, it is described using time information in the system state machine;
performing model checking on the model to be checked against the property to be checked, to automatically generate a trace that shows the model's evolution from its initial state to a state violating the property, wherein the trace represents the loss scenario, wherein the loss scenario comprises a process in which the system generates the system-level hazard.
2. The method according to claim 1 , wherein the system state machine comprises a controller state machine, a controlled process state machine, and an interaction between the controller state machine and the controlled process state machine.
3. The method according to claim 2 , wherein the system state machine comprises all behaviors of the controller, all behaviors of the controlled process, and all interactive behaviors between the controller and the controlled process, that are required for identifying the unsafe control action.
4. The method according to claim 1 , wherein the finite state machine incorporates a state machine nesting mechanism to represent a hierarchical control structure.
5. The method according to claim 1 , wherein identifying the loss scenario using model checking techniques and the identified unsafe control action comprises:
updating the system state machine, the updated system state machine comprising a controller state machine, a controlled process state machine, a sensor state machine, an actuator state machine, and an interaction thereof;
modeling a model checking model using the updated system state machine and identifying the loss scenario using the unsafe control action and the model checking model.
6. The method according to claim 5 , wherein the updated system state machine comprises all behaviors of the controller, all behaviors of the controlled process, all behaviors of the sensor, all behaviors of the actuator, and all behaviors of the interaction of the controller, the controlled process, the sensor, and the actuator, that are required for identifying the loss scenario.
7. The method according to claim 5 , wherein the system state machine is modeled using Systems Modeling Language (SysML), Architecture Analysis & Design Language (AADL) or AltaRica, and the model checking model is modeled using New Symbolic Model Verifier (NuSMV) or UPPAAL.
8. The method according to claim 1 , wherein the time information in the system state machine is described by a Modeling and Analysis of Real-Time and Embedded systems (MARTE) element or a clock variable.
9. The method according to claim 1 , wherein forming, based on the unsafe control action, a property to be checked using a model checking logic language comprises:
determining a system safety constraint based on the unsafe control action;
describing the system safety constraint using a model checking logic language to form a property to be checked.
10. The method according to claim 9 , wherein the generating a PUCA comprises:
determining the control action received by the controlled process and the context, using the system state machine, wherein the context comprises a state of the system;
identifying an instance of a combination of the control action received by the controlled process, the context and the type as the PUCA.
11. The method according to claim 1 , wherein the property to be checked is described using logic language Timed Computation Tree Logic (TCTL), Computation Tree Logic (CTL), Linear Temporal Logic (LTL), or Real-Time Computation Tree Logic (RTCTL).
12. A non-transitory computer readable storage medium comprising a computer program stored thereon, wherein the computer program implements the method of claim 1 when executed by a processor.
13. A computer device comprising a processor and a computer program, wherein the computer program implements the method of claim 1 when executed by the processor.