Automating Time Series Safety Analysis for Automotive Control Systems in STPA Using Weighted Partial Max-SMT

Recently, Systems-Theoretic Process Analysis (STPA) has been studied for automobile safety analysis. When STPA is used later in the design phase, significant effort is required to detect causal scenarios of unsafe control actions (UCAs), especially those related to intermittent disturbances in multiple signals. We propose a method to automate this disturbance detection by checking the satisfiability of trace formulas extended with cushion variables. At a state transition, cushion variable values are used instead of original variable values to determine the next state. A signal disturbance is regarded as assigning different values to variables and corresponding cushion variables. Specifying the equality between variables and cushion variables as soft clauses, a Weighted Partial Max-SMT solver mechanically searches an assignment for a trace to satisfy the UCA property. We applied the proposed technique to a simplified automotive control system to demonstrate some examples of automatic detections of reasonable intermittent multi-signal disturbances.