A new safety-guided design methodology to complement model-based safety analysis for safety assurance

Cyber-physical human systems are pervasive in today’s world. For example, the modern commercial airplane heavily depends on the collaboration of human pilot and cockpit automation to safely and efficiently transport passengers or cargo from Point A to Point B. Certifying a commercial airplane requires by law evidence that all the possible safety-critical scenarios that the airplane will encounter in the actual operation are adequately addressed, which is especially challenging for new aircraft entrants that have novel features (e.g., 737MAX) and future advanced air mobility concept. Similar challenges abound in many other cyber-physical human system domains, such as automated driving Kramer et al. (2020) and nuclear power plant Ahn et al. (2015).

With the rapid advancement of Formal Methods, Model-based Safety Analysis (MBSA) Sun et al. (2021) has been gaining tremendous attention for its ability to rigorously verify whether the safety-critical scenarios are properly addressed by a design solution. Many MBSA approaches have been developed over the past two decades. The prominent ones include AADL Feiler et al. (2006), AltaRica Prosvirnova (2014), and HipHops Kabir et al. (2018), which according to Bozzano et al. (2015), are the only three languages that “have matured beyond the level of research prototypes”. In general (Fig.1), these mainstream MBSA approaches start with a given design solution by formalizing it into a design model in the target languages; then faults and failures are modeled to achieve a safety model; finally, verification is conducted to see whether the given properties (functional or safety, deterministic or probabilistic) are satisfied.

However, there is a gap. Even assuming MBSA (or formal verification in a more general sense) can exhaustively check all the possible scenarios captured by the design solution, there are still open challenges. First, verification is already challenging for complex hybrid systems. More importantly, if certain safety-critical scenarios are not included or considered in the given design solution (the left shoulder of Fig.1), or the properties do not correctly reflect the hazard (the right shoulder of Fig.1), the results of MBSA cannot be fully trusted for safety assurance.

In fact, such a gap has already been identified by one of FAA’s reports Butka et al. (2015) that systems that pass formal verification can still be incorrect. Leveson (2020) further argues “formal verification can only show consistency between two formal models” and “cannot be used as a validation of acceptable safety”. Instead, Leveson proposes Systems Theoretic Process Analysis (STPA). STPA is known for its ability to identify hazardous scenarios associated with control Steck (2018) and define safety properties from the hazard Hobbs et al. (2021). Furthermore, STPA is also designed for analyzing systems with complex human-automation interactions Fleming and Leveson (2016), while the more traditional Fault Tree Analysis, as prescribed by ARP 4761 SAE (1996) for aviation certification, does not even consider humans or software in the fault tree, let alone analyzing the interaction between them. All these traits make STPA an ideal alternative to bridge this gap for cyber-physical human systems.

However, STPA has two weaknesses. First, STPA has to model an existing design solution into a control structure, which ultimately relies on the “art of modeling” and opens the window for inconsistency between the design model and the STPA model. Second, STPA provides less support in identifying the causes of the hazardous scenarios associated with control Leveson and Thomas (2013), which is why many approaches Kramer et al. (2020); Steck (2018) only use STPA to identify the safety-critical scenarios for the system as a whole, similar to, e.g., HAZOP. However, it is equally important to decompose these scenarios into more refined scenarios that the design solution can directly act upon. According to a recent review Zhang et al. (2021) on identifying the safety-critical scenarios in the Automated Driving community, no work is found that identifies the safety-critical scenarios to support defining the design solution.

Therefore, this paper proposes a new safety-guided design methodology, called STPA+, based on STPA to (1) derive the design solution directly and (2) provide better methodological support to identify and then address the safety-critical scenarios that the design solution should directly act upon. Because the safety-critical scenarios caused by failure have been addressed by MBSA (the bottom arrow in Fig.1), STPA+ only focuses on the safety-critical scenarios that happen without the presence of component-level failures. In fact, there is an ISO standard under development (ISO/PAS 21448, SOTIF) that specifically focuses on this type of scenarios. As a result, STPA+ strengthens the two shoulders of Fig.1, and “STPA+MBSA” provides more comprehensive safety assurance for cyber-physical human systems.

Finally, because STPA+ does not need an existing design solution to identify the safety-critical scenarios that a design solution should directly act upon, STPA+ can also be potentially used to design a run-time safety monitor for systems of which one has limited control over the operation, such as a legacy system or an AI-based system. The run-time monitor may function as a modular safety feature to capture hazardous scenarios and make decisions when the original system fails to act.

STPA+ shares the same system-theoretic view as STPA: a system can be abstracted as a (hierarchical) control structure (the left of Fig.2) regardless of a human controller, automation, or a team of both, which makes it an ideal candidate to design cyber-physical human systems.

A control structure operates in the following order (the red circle of Fig.2): (1) the controller observes the controlled process, (2) the controller issues control actions to manipulate the evolution of the controlled process, (3) the output behavior of the controlled process (called output behavior hereafter) achieves the functional goal and avoids the hazard.

Designing a control structure follows the opposite direction (the blue circle of Fig.2), which translates into the three methods of STPA+ below (the right of Fig.2).

• •

  Method 1: Translating the function/hazard into constraints on the output behavior. Because these constraints are the “desired end results” of the control structure as a whole, they are prescriptive constraints.

• •

  Method 2: Properly constraining a model of the controlled process. Because these constraints represent what the controlled process can possibly do, they are descriptive constraints.

• •

  Method 3: A reference architecture for the controller to issue the right control action at the right time so that the constraints from both directions will be respected.

The prescriptive constraints are defined on the output behavior. The output behavior comprises three elements: a start time $st$, a stop time $sp$, and the trajectory evolution in $[st,sp]$. Accordingly, constraints must be derived from the hazard for all three elements. Safety constraints in the current practice are mostly the restrictions on the trajectory evolution. For example, a minimal distance from the terrain is defined to constrain the descent of an airplane when it is descending. Such constraint on the trajectory evolution while the output behavior is ongoing is called performance constraint in this paper. However, the performance constraint does not prescribe when the output behavior should start or stop. The lack of constraints on the start/stop time may lead to the omission of safety-critical scenarios, especially for time-sensitive output behaviors. Therefore, the question is, how to derive the safety constraints on the start/stop time from the hazard.

First, consider the start time $st$. For example (Fig.3), a time-sensitive output behavior is safe to start only within $ST_{1}$ and $ST_{2}$, which divides the timeline into different sections with different meanings. The output behavior “must start” when the timeline comes to $ST_{1}$, otherwise the hazard will surely happen after $ST_{1}$; the output behavior “can start” when the timeline comes within $ST_{2}$, because if not, it can still start in $ST_{1}$; the output behavior “must not start” in the rest of the sections. Clearly, there are three types of constraints for the start time:

• •

  Must-start time window $mst\_T$: the output behavior must start within this time window, otherwise the hazard will happen after the time window expires.

• •

  Must-not-start time window $nst\_T$: the output behavior must not start within this time window, otherwise the hazard will happen immediately.

• •

  Can-start time window $cst\_T$: It is safe whether the intended output behavior starts or not when the time comes to $cst\_T$. Mathematically, the can-start time window is complementary to the $mst\_T$ and $nst\_T$, and can be calculated in (1), where $\mathcal{T}$ is the time before $mst\_T$ expires.

  $$cst\_T=\mathcal{T}\cap\neg(mst\_T\cup nst\_T)$$

  (1)

Second, we reason about the time windows. For the must-start condition, how can the hazard happen if the intended output behavior has not even started yet? That must be caused by the output behavior temporally immediately before the intended output behavior (called in-behavior hereafter) violating its own performance constraints (denoted as $pc^{i}$). For the must-not-start condition, the hazard is caused by the started intended output behavior violating its own performance constraints (denoted as $pc$). Therefore, the must-start time window is defined to avoid the in-behavior from stopping at the wrong time to violate $pc^{i}$; the must-not-start time window is to avoid the intended output behavior from starting at the wrong time to violate $pc$.

Taking merging into the traffic for example, with the in-behavior and the intended output behavior and their respective performance constraints defined in Fig.4. The “must-start” time window is determined based on the time left before the car breaches the minimal distance from the end of the merge lane (i.e., the in-behavior violating $pc^{i}$). The “must-not-start” time window is determined based on the time when there is no safe opening to merge into the traffic (i.e., the intended output behavior violating $pc$).

As a result, the constraints on the start/stop time can be summarized in Fig.5. The must-start, must-not-start and can-start time window ($mst\_T,nst\_T$ and $cst\_T$) are derived based on the performance constraints of the in-behavior $pc^{i}$ and the performance constraints of the intended output behavior $pc$. Similarly, the must-stop, must-not-stop and can-stop time window ($msp\_T,nsp\_T$ and $csp\_T$) are derived based on $pc$ and the performance constraints of the out-behavior $pc^{o}$. Eventually, the prescriptive constraints of the output behavior $y(t)$ where $t\in[st,sp]$ can be defined in (2), and $Y(t),ST$ and $SP$ are the final prescriptive constraints.

Method 2 is to constrain a model of the controlled process properly. An incorrect model can lead to hazardous scenarios that will escape the scrutiny of any model-based analysis. General System Theory Mesarovic and Takahara (1975) provides a generic construct $(u(t),x(t),p)\xrightarrow{f}(\dot{x},y(t))^{T}$ to model the controlled process, where $u$ is the control, $p$ is the set of parameters, $x$ is the system state, and $y$ is the output. Since the basic construct can only be determined case-by-case,the question is, how to properly constrain a given construct $(f,u,x,p,\dot{x},y)$ for a controlled process?

Fig.6 provides a map to identify the constraints. Each dotted arrow may yield both the constraints on $(u,x,p,\dot{x},y)$ and the associated assumptions on the environment and the system/human.

First, $f$ represents concrete mechanisms (engineered or natural) of the actual process. It may only be able to process a finite set of the inputs and hence have constraints on the inputs (Arrow 1).

Second, the controlled process operates on actual components. For those that are out of the design scope (i.e., the designer has no control), we call them “environment”. Components within the design scope are the “system” to be built or further refined, or “human” to be trained. For the environment, it may have a set that includes all the possible inputs (Arrow 2) and another set in which all the possible outputs must be included (Arrow 3). For the system/human, it is always subject to finite design/manufacture/natural capacities that may yield constraints on both inputs and outputs (Arrow 4).

Third, $(u,x,p,\dot{x},y)$ is internally constrained by $f$. Therefore, the constraints on $(u,x,p,\dot{x},y)$ also need to satisfy $f$ mathematically (Arrow 5).

Finally, each constraint may have assumptions on the environment and the system/human for the constraint to be valid in the first place. Therefore, constraints and assumptions should always appear in pairs, and any isolated constraint or assumption must be justified.

Therefore, all the constraint-assumption pairs (denoted as {constraint$|$ assumption on system/human$|$ assumption on environment}) need to be identified based on Fig.6 to properly constrain the model of the controlled process. For example (Fig.7), Vehicle A (an eVTOL) is instructed to descend to Point W with a constant descent angle $\gamma$. We treat $\gamma$ as a system state and derive its constraint-assumptions pair based on Fig.6. Note that Arrow 2 and Arrow 5 do not apply to this example.

As a result, the constraints of $\gamma$ are $\Gamma_{1}\cap\Gamma_{3}\cap\Gamma_{4}$, and the associated assumptions are $BL\wedge CW\wedge Nom\wedge PD\wedge EL$.

Finally, the same procedure is applied to each element of $(u,x,p,\dot{x},y)$ for the constraint-assumption pair. Eventually, the descriptive constraints can be represented in (3), where $AS$ is the set of the assumptions.

Mathematically, the next task is to design a controller to find the control actions to satisfy the constraints from (2) and (3). However, a safe controller in an actual system is more than a mathematical problem solver. It is a decision-maker that constantly monitors the environment and the controlled process, watches out for hazards, reacts to changes, and adjusts the decisions in real-time. To design such a safe controller is to identify all the safety-critical scenarios and design mechanisms into the controller to address them accordingly.

First, a controller in the most general sense, must make the following three decisions.

1. 1.

   Decide prescriptive constraints: In a dynamic environment, what is safe/unsafe usually changes in real-time. The controller must adjust the prescriptive constraints accordingly.

2. 2.

   Decide control reference: Because the controller needs control references to generate the control action, this decision is to decide the control references from the prescriptive constraints.

3. 3.

   Decide control action: This decision is akin to the control algorithm in traditional feedback control: generating control actions from given control references.

Taking “lane merging” in Fig.4 for example, Decision (1) is to find the road section and time window to merge safely by monitoring the traffic; Decision (2) is to decide the specific position and time to merge; Decision (3) is to operate the steering and gas to execute the merge.

Second, regardless of the decision being made, there are five types of unsafe scenarios (without failure/fault) when making a decision (Fig.8). (i) No-decision refers to the scenarios where no decision can be found. (ii)Previously safe refers to the scenarios where an already generated decision becomes unsafe due to change. (iii)Unsafe timing refers to the scenarios where the decision is made too late, so much so the timing constraints in (2) cannot be met as the operation of the rest of the system also takes time. (iv)Time coupling refers to the scenarios where the result of a decision is affected by the time delay of the system, i.e., time and value are coupled, such as the phenomenon of Pilot-induced Oscillations. (v)Wrong math refers to the scenarios where the algorithm to calculate the decision is wrong or inadequate. Most works in theoretical control or formal methods are to get the math right. Therefore, we do not consider this scenario in the reference architecture. All the unsafe scenarios above are scenarios, if not appropriately addressed, can cause a hazard.

Third, we consider how the safety-critical scenarios explained above (except the“wrong math”) can happen to each of the three decisions that a controller makes. We will continue using the “lane merging” as a running example for the first two decisions.

Finally, the scenarios identified above can already be used to examine whether an existing controller design is safe. However, STPA+ takes one step further by defining sub-decisions within each decision to address all the safety-critical scenarios. Although the details are out of the scope of this paper, we define 33 main sub-decisions, 12 enabling sub-decisions, and their interactions as a reference architecture. The reference architecture works like a class (as in Object-Oriented Programming). In the specific design applications, engineers only need to instantiate the reference architecture and tailor it for their own problems, yielding a controller that has all the safety-critical scenarios (without component-level failure) automatically addressed. We will explain the details of the reference architecture in an extension of this work.

MBSA has gained tremendous traction over the past two decades due to its ability to rigorously prove whether all the safety-critical scenarios captured in the design solution are addressed correctly. However, to apply MBSA for certification of safety-critical systems, one still needs to demonstrate that the model used in MBSA includes all the possible safety-critical scenarios that the actual system will encounter in actual operation. Current MBSA approaches are not equipped for this task.

To tackle this problem, we propose a new safety-guided design methodology, called STPA+, to complement MBSA for safety assurance. STPA+ treats a system as a control structure, which is particularly fit for systems with complex interactions between human, machine, and automation. Furthermore, STPA+ comprises three methods. Method 1 is to derive safety constraints from the hazard to make sure the safety constraints adequately reflect the hazard under study. Method 2 is to define the model of the controlled process to make sure the model is properly constrained both explicitly and implicitly. Method 3 is to define a safe controller (human, automation, or a team of both) by providing a reference architecture to make sure the controller defined based on the reference architecture has all the safety-critical scenarios (without component-level failure) addressed. In summary, Method 1 strengthens the right shoulder of Fig.1; Method 2&3 strengthens the left shoulder of Fig.1. Together, “STPA+MBSA” provides a strong and comprehensive argument for the safety assurance of a cyber-physical human system.

In the future, we will demonstrate specifically how STPA+ can address the concerns in ISO/PAS 21448 (Safety of the intended functionality). Moreover, because STPA+ does not require knowledge about the design solution to identify the safety-critical scenarios that a controller must directly act on, we will apply STPA+ to design a run-time monitor as a modular safety feature to assist the human/AI-based controller or the automation controller of a legacy system to capture and act on hazardous scenarios when necessary.