| CPC G05B 23/0243 (2013.01) [G05B 23/0235 (2013.01); G05B 23/0275 (2013.01)] | 13 Claims |

|
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.
|