시스템 이론적 프로세스 분석 (System-Theoretic Process Analysis, STPA)은 광범위한 안전 필수 시스템 (safety-critical systems)에 적용되어 온 잘 확립된 위험 분석 기법입니다. 이러한 인기에도 불구하고, STPA를 위한 자동화 지원은 상대적으로 적으며, 대부분의 단계가 인간 분석가에 의해 수동으로 수행되는데, 이는 많은 시간이 소요되고 오류가 발생하기 쉽습니다. 본 논문은 인간 분석가가 STPA를 효율적이고 정확하게 수행할 수 있도록 돕기 위해 모델 기반 공학 (model-based engineering) 및 형식 기법 (formal methods)의 잠재적 활용을 조사합니다. FASR (Formalizing and Automating STPA with Robustness)이라 불리는 제안된 도구는 강건성 분석 (robustness analysis)의 최근 발전을 활용하여 제어기 동작의 바람직하지 않은 편차 (undesirable deviations)로서 불안전한 제어 동작 (unsafe control actions, UCAs)을 식별함으로써, UCAs의 자동화된 완전한 식별을 가능하게 합니다. 이 도구의 사용은 항공 전자 시스템 (avionics system)의 제동 시스템 제어 장치 (Braking System Control Unit, BSCU)를 포함하는 사례 연구를 통해 입증되었습니다. 도구의 잠재적 이점과 한계에 대한 예비 탐색으로서, 본 논문은 STPA, 모델 기반 공학, 그리고 형식 기법에 대해 다양한 배경을 가진 9명의 참가자가 참여한 사용자 연구를 보고합니다. 연구 결과, 대부분의 참가자는 이 도구가 UCAs를 식별하는 데 유용한 보조 도구라고 간주하였으며, 동시에 FASR와 같은 도구가 더 넓은 범위의 시스템과 분석가에게 사용 가능하고 적용 가능하게 만들기 위한 개선 사항들을 제안하였습니다.