[Paper] FASR: Automated Identification of Unsafe Control Actions in STPA

Source: arXiv - 2605.30697v1

Overview

The paper presents FASR, a prototype tool that brings model‑based engineering and formal verification to the System‑Theoretic Process Analysis (STPA) workflow. By automatically enumerating unsafe control actions (UCAs) for a given controller model, FASR aims to cut down the manual, error‑prone effort that safety analysts traditionally invest in STPA—especially for complex cyber‑physical systems such as avionics.

Key Contributions

• Formalization of STPA’s UCA identification as a robustness‑analysis problem, enabling systematic, exhaustive search for unsafe actions.
• FASR toolchain that integrates a high‑level system model (e.g., Simulink/Stateflow) with a SAT/SMT‑based robustness engine to automatically generate UCAs.
• Empirical evaluation through a case study on an Avionics Braking System Control Unit (BSCU) and a user study with nine participants from diverse backgrounds.
• Design guidelines for making formal STPA assistance usable by analysts with limited formal‑methods expertise.

Methodology

1. Model Extraction – The target controller (e.g., a BSCU) is modeled in a standard engineering language (Simulink/Stateflow). FASR extracts a transition system that captures all possible controller actions under different input conditions.
2. Robustness Specification – Unsafe control actions are expressed as undesirable deviations from intended outputs (e.g., “apply brake when speed < 5 km/h”). These are encoded as logical constraints.
3. Automated Search – Using a SAT/SMT solver, FASR performs a robustness analysis: it searches for input scenarios that force the controller to violate the constraints, thereby producing concrete UCAs together with the triggering context.
4. Result Presentation – The tool maps each found UCA back to the original model, showing the exact state‑space path and the offending control signal, which analysts can then review and refine.

The approach is deliberately kept model‑agnostic: any controller that can be expressed as a finite‑state transition system can be fed into FASR.

Results & Findings

• Case Study (BSCU) – FASR discovered 12 distinct UCAs, including several that were missed in the original manual STPA effort. The tool produced traceable counter‑examples in under 30 seconds.
• User Study – 7 out of 9 participants reported that FASR significantly reduced the time needed to identify UCAs. Participants with limited formal‑methods background still found the generated reports understandable after a brief tutorial.
• Error Reduction – Analysts using FASR reported fewer false positives/negatives compared with a purely manual approach, suggesting that exhaustive search mitigates human oversight.

Practical Implications

• Faster Hazard Analyses – Development teams can integrate FASR early in the design cycle to automatically flag unsafe control logic before costly hardware prototypes are built.
• Continuous Safety Assurance – Because the tool works on the same model used for simulation and code generation, it can be run automatically in CI pipelines, providing regression‑style safety checks whenever the controller changes.
• Cross‑Domain Applicability – While demonstrated on avionics, the underlying robustness formulation works for automotive ECUs, robotics controllers, and IoT edge devices, making it a reusable safety‑analysis asset.
• Skill Barrier Lowering – By surfacing concrete counter‑examples rather than raw formal specifications, FASR lets engineers without deep theorem‑proving expertise participate in STPA, fostering broader safety culture.

Limitations & Future Work

• Model Fidelity – FASR’s completeness hinges on the accuracy of the extracted transition system; abstractions that omit timing or stochastic behavior may hide some UCAs.
• Scalability – The SAT/SMT search can explode for very large state spaces; the authors note the need for compositional or heuristic pruning techniques.
• User Interface – Participants suggested richer visualizations (e.g., overlaying UCAs on Simulink block diagrams) and tighter integration with existing safety‑analysis tools.
• Broader Validation – Future work includes applying FASR to larger, multi‑controller systems and conducting longitudinal studies to measure impact on real‑world certification processes.

Authors

• Ian Dardik
• Yining She
• Sam Procter
• Keaton Hanna
• Lutz Wrage
• Eunsuk Kang

Paper Information

• arXiv ID: 2605.30697v1
• Categories: cs.CR, cs.SE
• Published: May 29, 2026
• PDF: Download PDF