The System-Theoretic Process Analysis (STPA) is a well-established hazard analysis technique that has been applied to a wide range of safety-critical systems. Despite its popularity, there is relatively little automation support for STPA, and most of its steps are carried out manually by a human analyst, which can be time consuming and error prone. This paper investigates the potential use of model-based engineering and formal methods to assist human analysts in efficiently and accurately carrying out STPA. The proposed tool, called FASR (Formalizing and Automating STPA with Robustness), enables automated, complete identification of unsafe control actions (UCAs), leveraging recent advances in robustness analysis to identify UCAs as undesirable deviations in the controller's actions. The use of the tool is demonstrated on a case study involving a Braking System Control Unit (BSCU) in an avionics system. As a preliminary exploration of the potential benefits and limitations of the tool, the paper reports on a user study involving nine participants with varying backgrounds in STPA, model-based engineering, and formal methods; the study found that most participants considered the tool a useful aid in identifying UCAs, while suggesting improvements that would make a tool such as FASR usable and applicable to a wider range of systems and analysts.

翻译：系统理论过程分析（STPA）是一种成熟的事故分析技术，已广泛应用于各类安全关键系统。尽管该方法广受欢迎，但支持STPA的自动化工具相对匮乏，其大多数步骤仍需人工分析师手动执行，既耗时又易出错。本文研究了基于模型的工程与形式化方法在帮助人工分析师高效、准确地执行STPA方面的潜在应用。所提出的工具FASR（基于鲁棒性的STPA形式化与自动化）能够自动、完整地识别不安全控制行为，该方法利用鲁棒性分析的最新进展，将不安全控制行为识别为控制器动作中不可接受的偏差。通过在航空电子系统中的制动系统控制单元（BSCU）案例研究，展示了该工具的应用。作为对工具潜在优势与局限性的初步探索，本文报告了一项涉及九名参与者的用户研究，这些参与者具备不同水平的STPA、基于模型的工程及形式化方法背景。研究发现，大多数参与者认为该工具有助于识别不安全控制行为，同时提出了改进建议，以使FASR这类工具更易于使用并适用于更广泛的系统与分析师群体。