pith. sign in

arxiv: 2605.30697 · v1 · pith:ZDECU75Dnew · submitted 2026-05-29 · 💻 cs.CR · cs.SE

FASR: Automated Identification of Unsafe Control Actions in STPA

Ian Dardik , Yining She , Sam Procter , Keaton Hanna , Lutz Wrage , Eunsuk Kang This is my paper

Pith reviewed 2026-06-28 22:23 UTC · model grok-4.3

classification 💻 cs.CR cs.SE
keywords STPAunsafe control actionsautomationformal methodsrobustness analysissafety-critical systemsavionicsmodel-based engineering
0
0 comments X

The pith

FASR automates complete identification of unsafe control actions in STPA by detecting them as robustness deviations in controller actions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces the FASR tool to automate the identification of unsafe control actions, a key manual step in the System-Theoretic Process Analysis method used for safety-critical systems. STPA analysts currently spend significant effort labeling control actions as unsafe based on context, which can lead to inconsistencies or omissions. FASR builds formal models of the controller and plant, then applies robustness analysis to flag undesirable deviations automatically. The approach is shown on a braking system control unit from an avionics example, and a user study with nine participants indicates most found the output helpful as an aid.

Core claim

FASR enables automated, complete identification of unsafe control actions by leveraging recent advances in robustness analysis to identify UCAs as undesirable deviations in the controller's actions, demonstrated through a case study on a Braking System Control Unit in an avionics system.

What carries the argument

FASR tool, which combines formal models of controller and plant with robustness analysis to detect unsafe control actions as action deviations.

If this is right

  • STPA analysis becomes faster and less error-prone when UCA identification is automated.
  • The tool produces complete results for systems that admit formal controller-plant models, such as the avionics BSCU example.
  • Analysts with mixed backgrounds in STPA and formal methods can use the output as a reliable starting point.
  • Further tool refinements are required before the method applies to a wider range of systems and analyst skill levels.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same robustness-based deviation detection could be adapted to other hazard analysis methods that rely on identifying unsafe behaviors.
  • Early-stage design might still require manual STPA because formal models are often unavailable until later phases.
  • Combining FASR output with existing model-based engineering environments could reduce the barrier to adoption.

Load-bearing premise

A formal model of the controller and plant, together with robustness analysis, can capture all the context and intent that a human STPA analyst would use to decide whether a control action is unsafe.

What would settle it

An unsafe control action present in the Braking System Control Unit case study that FASR fails to report, or a participant in the user study who cannot complete UCA identification with the tool.

Figures

Figures reproduced from arXiv: 2605.30697 by Eunsuk Kang, Ian Dardik, Keaton Hanna, Lutz Wrage, Sam Procter, Yining She.

Figure 1
Figure 1. Figure 1: (A) Control structure and sample (B) unsafe control actions for the Braking System Control Unit (BSCU) case study [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A screenshot of Cameo Enterprise Architecture (CEA) showing the BSCU case study modeled using the SysML profile created for this effort. (A) is a state machine diagram of the BSCU, (B) is an activity diagram of the crew instructions, (C) is the hazard we want to avoid, expressed as an invariant. example system described in, among other publications, the STPA Handbook [16]. This case study captures a scenar… view at source ↗
Figure 3
Figure 3. Figure 3: An overview of the FASR tool. 1(B) identifies that a hazard may occur if the flight crew fails to arm the BSCU before landing, which is required by the BSCU instruction manual. UCA Identification with FASR. Ordinarily, an STPA analyst must man￾ually identify the UCAs in the third step. In this paper, we advocate assisting UCA identification with an automated tool such as FASR. A key advantage to this appro… view at source ↗
Figure 4
Figure 4. Figure 4: An excerpt of the UCA table generated by FASR for the BSCU example. Time (sec) Generated UCAs Fortis Cold Warm Fortis Filtered States Trans. BSCU, No Abnormal Behavior 4.7 4.1 31 14 241 3100 BSCU, With Abnormal Behavior 7.5 5.8 55 23 1249 50024 [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The manuscript proposes the FASR tool to automate identification of unsafe control actions (UCAs) in STPA. It models the controller and plant formally and applies robustness analysis to detect undesirable deviations from nominal controller behavior as UCAs. The approach is demonstrated via a Braking System Control Unit (BSCU) case study in avionics; a user study with nine participants of varying STPA and formal-methods backgrounds reports that most found the tool useful, while noting needed improvements for broader applicability.

Significance. If the completeness claim is substantiated, the work offers a concrete direction for reducing manual effort and inconsistency in STPA, a widely used hazard-analysis method. The combination of model-based engineering with robustness analysis is a promising technical step. The user study provides initial qualitative evidence of usability. However, the absence of any quantitative validation (recall, precision, or direct comparison to manual UCA tables) substantially limits the demonstrated significance of the central automation claim.

major comments (3)
  1. [Abstract] Abstract: the claim of 'automated, complete identification of unsafe control actions' is load-bearing for the paper's contribution, yet no quantitative metrics (recall against a ground-truth manual STPA analysis, false-positive rate, or coverage of context-sensitive hazards) are reported for the BSCU example.
  2. [§4] §4 (BSCU case study): the demonstration does not include a side-by-side enumeration or table comparing the UCAs returned by the robustness procedure against those that would be identified by a conventional manual STPA analyst considering the same hazards, environmental context, and system intent.
  3. [§5] §5 (user study): the study measures only perceived usefulness and suggested improvements; it supplies no data on whether FASR recovers every manually identified UCA or introduces spurious ones, leaving the weakest assumption (that robustness deviations capture all analyst context and intent) untested.
minor comments (2)
  1. [Abstract] Abstract: the expansion of the FASR acronym ('Formalizing and Automating STPA with Robustness') is given only in the abstract; repeating it once in the introduction would aid readers.
  2. The manuscript would benefit from an explicit statement of the modeling assumptions required for the controller/plant formalization (e.g., discrete vs. continuous time, scope of environmental disturbances) so that readers can assess applicability to other systems.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the constructive and detailed comments, which help clarify the scope and limitations of our preliminary work on FASR. We address each major comment below, indicating planned revisions where appropriate. The manuscript presents an initial exploration combining formal robustness analysis with STPA; we agree that stronger quantitative evidence would strengthen the automation claims.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim of 'automated, complete identification of unsafe control actions' is load-bearing for the paper's contribution, yet no quantitative metrics (recall against a ground-truth manual STPA analysis, false-positive rate, or coverage of context-sensitive hazards) are reported for the BSCU example.

    Authors: We acknowledge that the abstract's phrasing of 'automated, complete identification' is strong and that the BSCU demonstration provides only an illustrative application rather than quantitative validation metrics such as recall or precision. The completeness claim rests on the formal coverage of robustness violations within the modeled controller-plant interface, but we agree this does not substitute for empirical comparison against manual analysis. We will revise the abstract to qualify the claim (e.g., 'automated identification of UCAs as robustness violations') and add an explicit limitations paragraph discussing the absence of such metrics. revision: yes

  2. Referee: [§4] §4 (BSCU case study): the demonstration does not include a side-by-side enumeration or table comparing the UCAs returned by the robustness procedure against those that would be identified by a conventional manual STPA analyst considering the same hazards, environmental context, and system intent.

    Authors: The BSCU case study serves to demonstrate tool usage on a realistic avionics example rather than to perform exhaustive validation. A direct side-by-side table would require an independent, fully documented manual STPA by domain experts on the identical hazard set and context, which exceeds the scope of this initial study. We will add a new subsection in §4 that enumerates the UCAs produced by FASR, discusses how they relate to the modeled hazards, and explicitly notes the lack of a manual baseline comparison as a limitation. revision: partial

  3. Referee: [§5] §5 (user study): the study measures only perceived usefulness and suggested improvements; it supplies no data on whether FASR recovers every manually identified UCA or introduces spurious ones, leaving the weakest assumption (that robustness deviations capture all analyst context and intent) untested.

    Authors: The user study was intentionally scoped as a preliminary qualitative assessment of perceived usefulness across participants with mixed STPA and formal-methods backgrounds; it was not designed as a controlled accuracy evaluation. We agree that this leaves the assumption that robustness deviations fully capture analyst intent untested in quantitative terms. In revision we will expand §5 and the conclusions to state this limitation clearly and to outline the design of a future controlled study that would measure recall/precision against manual UCA tables. revision: yes

Circularity Check

0 steps flagged

No circularity: tool description and case study lack any derivation chain or fitted predictions

full rationale

The paper describes a software tool (FASR) that applies existing robustness analysis techniques to formal controller/plant models in order to flag unsafe control actions. No equations, parameter fits, uniqueness theorems, or predictive claims appear in the provided text. The completeness argument is presented as an empirical claim evaluated via case study and user study rather than derived from prior self-citations or by construction. The mapping from robustness deviations to STPA UCAs is treated as an engineering assumption, not a mathematical reduction that collapses to the inputs. This is the normal non-circular outcome for a tool-building paper without a formal derivation.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract supplies no information on free parameters, background axioms, or new postulated entities.

pith-pipeline@v0.9.1-grok · 5769 in / 991 out tokens · 21412 ms · 2026-06-28T22:23:41.843277+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

25 extracted references

  1. [1]

    Risk Analysis and Assessment Modeling Language (RAAML) Libraries and Pro- files Version 1.1 Beta 2. Tech. Rep. ptc/24-03-02, OMG Standards Development Organization (March 2024)

    2024

  2. [2]

    Procedia Engineering128, 2–11 (2015), proceedings of the 3rd European STAMP Workshop

    Abdulkhaleq, A., Wagner, S., Leveson, N.: A comprehensive safety engineering approach for software-intensive systems based on stpa. Procedia Engineering128, 2–11 (2015), proceedings of the 3rd European STAMP Workshop

    2015

  3. [3]

    In: 2022 IEEE International Symposium on Systems Engineering (ISSE)

    Ahlbrecht, A., Zaeske, W., Durak, U.: Model-Based STPA: Towards Agile Safety- Guided Design with Formalization. In: 2022 IEEE International Symposium on Systems Engineering (ISSE). pp. 1–8 (Oct 2022), iSSN: 2687-8828

    2022

  4. [4]

    In: 2013 ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS)

    Asare, P., Lach, J., Stankovic, J.A.: Fstpa-i: A formal approach to hazard identi- fication via system theoretic process analysis. In: 2013 ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS). pp. 150–159 (2013)

    2013

  5. [5]

    In: Formal Methods for the Design of Real-Time Systems

    Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Formal Methods for the Design of Real-Time Systems. LNCS, vol. 3185, pp. 200–236. Springer, Berlin, Heidelberg (2004)

    2004

  6. [6]

    In: Proceedings of the 21st Safety-Critical Systems Symposium

    Colley, J., Butler, M.: A formal, systematic approach to stpa using event-b refine- ment and proof. In: Proceedings of the 21st Safety-Critical Systems Symposium. Safety-Critical Systems Club, Bristol, UK (February 2013)

    2013

  7. [7]

    Safety Science109, 130–143 (2018)

    Dakwat, A.L., Villani, E.: System safety assessment based on stpa and model checking. Safety Science109, 130–143 (2018)

    2018

  8. [8]

    Damerau, F.J.: A technique for computer detection and correction of spelling er- rors. Commun. ACM7(3), 171–176 (Mar 1964)

    1964

  9. [9]

    3ds.com/products/catia/no-magic/cameo-enterprise-architecture, 2024x

    Dassault Syst` emes: Cameo Enterprise Architecture (January 2026),https://www. 3ds.com/products/catia/no-magic/cameo-enterprise-architecture, 2024x

    2026

  10. [10]

    IEEE Access10, 120936– 120950 (2022)

    De Saqui-Sannes, P., Vingerhoeds, R.A., Garion, C., Thirioux, X.: A Taxonomy of MBSE Approaches by Languages, Tools and Methods. IEEE Access10, 120936– 120950 (2022)

    2022

  11. [11]

    John Wiley & Sons, Inc., Fredericksburg, Virginia, United States of America, second edn

    Ericson II, C.A.: Hazard Analysis Techniques for System Safety. John Wiley & Sons, Inc., Fredericksburg, Virginia, United States of America, second edn. (2016)

    2016

  12. [12]

    Galois, Inc: Camet tools (2025),https://tools.galois.com/camet/overview/ camet-tools, Last accessed on 2026-03-03

    2025

  13. [13]

    In: ERTS 2022

    Hetherington, D., Roques, P.: STPA Analysis of Automotive Safety Using Arcadia and Capella. In: ERTS 2022. pp. 191–200. HAL Open Science, Toulouse, France (Jun 2022)

    2022

  14. [14]

    Nuclear Engineering and Technology54(5), 1635–1643 (May 2022)

    Jung, S., Heo, Y., Yoo, J.: A formal approach to support the identification of unsafe control actions of STPA for nuclear protection systems. Nuclear Engineering and Technology54(5), 1635–1643 (May 2022)

    2022

  15. [15]

    Addison-Wesley (6 2002)

    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (6 2002)

    2002

  16. [16]

    Leveson, N., Thomas, J.: STPA Handbook. Tech. rep. (2018)

    2018

  17. [17]

    OMG ® Systems Modeling: OMG Systems Modeling Language™(SysML ®) ver- sion 1.7. Tech. Rep. formal/24-01-07, OMG Standards Development Organization (January 2024)

    2024

  18. [18]

    In: Gallina, B., T¨ orngren, M., Bitsch, F

    Petzold, J., von Hanxleden, R.: Hot PASTA: Improved Pragmatics for System- Theoretic Process Analysis. In: Gallina, B., T¨ orngren, M., Bitsch, F. (eds.) Com- puter Safety, Reliability, and Security. pp. 160–174. Springer Nature Switzerland, Cham (2026)

    2026

  19. [19]

    In: 18th Annual Symposium on Foun- dations of Computer Science (sfcs 1977)

    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foun- dations of Computer Science (sfcs 1977). pp. 46–57 (1977)

    1977

  20. [20]

    In: 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014 (2014)

    Procter, S., Hatcliff, J.: An architecturally-integrated, systems-based hazard anal- ysis for medical applications. In: 12th ACM/IEEE International Conference on Methods and Models for System Design, MEMOCODE 2014 (2014)

    2014

  21. [21]

    In: Gl¨ asser, U., Creissac Campos, J., M´ ery, D., Palanque, P

    Salehi Fathabadi, A., Snook, C., Dghaym, D., Hoang, T.S., Alotaibi, F., Butler, M.: Designing critical systems using hierarchical stpa and event-b. In: Gl¨ asser, U., Creissac Campos, J., M´ ery, D., Palanque, P. (eds.) Rigorous State-Based Methods. pp. 220–237. Springer Nature Switzerland, Cham (2023)

    2023

  22. [22]

    In: 2020 IEEE International Systems Conference (SysCon)

    de Souza, F.G.R., de Melo Bezerra, J., Hirata, C.M., de Saqui-Sannes, P., Apvrille, L.: Combining stpa with sysml modeling. In: 2020 IEEE International Systems Conference (SysCon). pp. 1–8 (2020)

    2020

  23. [23]

    In: Proceedings of the Twenty- first Safety-Critical Systems Symposium

    Thomas, J., Leveson, N.: Generating formal model-based safety requirements for complex, software- and human-intensive systems. In: Proceedings of the Twenty- first Safety-Critical Systems Symposium. Safety-Critical Systems Club, Bristol, United Kingdom (2013)

    2013

  24. [24]

    In: Formal Methods in Computer- Aided Design (FMCAD)

    Zhang, C., Dardik, I., Meira-G´ oes, R., Garlan, D., Kang, E.: Fortis: A tool for analysis and repair of robust software systems. In: Formal Methods in Computer- Aided Design (FMCAD). pp. 1–9. IEEE (2023)

    2023

  25. [25]

    In: Proceedings of ESEC/FSE

    Zhang, C., Garlan, D., Kang, E.: A behavioral notion of robustness for software systems. In: Proceedings of ESEC/FSE. p. 1–12 (2020)

    2020