Computer Science

Computer Science ›› 2026, Vol. 53 ›› Issue (1): 341-352.doi: 10.11896/jsjkx.241000156

• Information Security • Previous Articles     Next Articles

Research on Safety Analysis of Mode Transition of Flight Guidance System Based on STPA

ZUO Chencui, HUANG Zhiqiu, HU Jun, XIE Jian, XU Heng, SHI Fan   

  1. School of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
  • Received:2024-10-28 Revised:2025-03-10 Published:2026-01-08
  • About author:ZUO Chencui,born in 2000,postgra-duate.Her main research interests include formal methods and system safety analysis.
    HUANG Zhiqiu,born in 1965,Ph.D,professor,is a distinguished member of CCF(No.09028D).His main research interests include software engineering,safety of software and formal methods.
  • Supported by:
    Joint Funds of the National Natural Science Foundation of China(U224120044).

PDF (PC)

4

Abstract: In the process of automatic flight of civil aircraft,the mode transition of the flight guidance system is an important factor affecting safety and should be subject to a comprehensive safety analysis.Traditional safety analysis methods mainly focus on the failure factors of individual components,ignoring the safety issues arising from the nonlinear interactions between components.For this reason,this paper adopts the System Theory Process Analysis(STPA) method to conduct a systematic and complete analysis of the mode transition of the flight guidance system.Meanwhile,considering that there are parts in the STPA me-thod that require manual analysis,the formal model checking tool UPPAAL based on the theory of timed automata is introduced to model and verify the system,so as to ensure the correctness of the control structure diagram and identify the truly Unsafe Control Actions(UCA),thus avoiding the waste of resources.Finally,a standardized causal factor analysis framework is proposed to analyze the verified UCAs one by one.The example proves that the proposed method is effective for the safety analysis of aviation complex systems.

Key words: Flight guidance system, Mode transition, System theoretic process analysis, Model checking, UPPAAL

CLC Number: 

  • V249
[1]SAVELEV A,NERETIN E.Development of safetyrequire-ments for tracking active pilot controls by signals from an automatic flightcontrol system[C]//Proceedings of the 2019 International Conference on Control,Artificial Intelligence,Robotics &Optimization(ICCAIRO).IEEE,2019:19-24.
[2]OLIVER N,CALVARD T,POTOČNIK K.Cognition,technology,and organizational limits:Lessons from the Air France 447 disaster[J].Organization Science,2017,28(4):729-743.
[3]BOSS K K.Characteristics and analysis of major US air carrier accidents between 1991 and 2010[M].Oklahoma:Oklahoma State University,2012.
[4]LI X,ZHU Y,FAN Y,et al.A Comparison of SAE ARP 4754A and ARP 4754[J].Procedia Engineering,2011,17:400-406.
[5]LEVESON N,FLEMING C,THOMAS J,et al.A Comparison of SAE ARP 4761 and STPA Safety Assessment Processes[C]//Safety-Critical Systems Symposium.2015.
[6]QIE Z,YAN H.A Causation Analysis of Chinese Subway Construction Accidents Based on Fault Tree Analysis-Bayesian Network[J].Frontiers in Psychology,2022,13:887073.
[7]ANJALEE J A L,RUTTER V,SAMARANAYAKE N R.Application of failure mode and effect analysis(FMEA) to improve medication safety:a systematic review[J].Postgraduate Medical Journal,2021,97(1145):168-174.
[8]MILLER S P,CARLSON T M,TRIBBLE A C.Flight guidance system requirements specification[R].NASA,2003.
[9]TRIBBLE A C,LEMPIA D L,MILLER S P.Software safetyanalysis of a flight guidance system[C]//Proceedings of the 21st Digital Avionics Systems Conference.IEEE,2002.
[10]JOSHI A,MILLER S P,HEIMDAHL M P E.Mode confusion analysis of a flight guidance system using formal methods[C]//Digital Avionics Systems Conference.2003.
[11]OWRE S,RUSHBY J M,SHANKAR N.PVS:A prototype ve-rification system[C]//International Conference on Automated Deduction.Berlin:Springer,1992:748-752.
[12]CIMATTI A,CLARKE E,GIUNCHIGLIA F,et al.NuSMV:A new symbolic model verifier[C]//Computer Aided Verification:11th International Conference.Berlin:Springer,1999:495-499.
[13]WOODCOCK J,LARSEN P G,BICARREGUI J,et al.Formal methods:Practice and experience[J].ACM Computing Surveys,2009,41(4):1-36.
[14]SULAMAN S M,BEER A,FELDERER M,et al.Comparison of the FMEA and STPA safety analysis methods-a case study[J].Software Quality Journal,2019,27:349-387.
[15]LEVESON N G.Engineering a safer world:Systems thinkingapplied to safety[M]. Massachusetts:MIT Press,2016.
[16]LEVESON N,DULAC N,ZIPKIN D,et al.Engineering resilience into safety-critical systems[M]//Resilience Engineering.2017:95-123.
[17]CHAAL M,BANDA O A V,GLOMSRUD J A,et al.A framework to model the STPA hierarchical control structure of an autonomous ship[J].Safety Science,2020,132:104939.
[18]SAHAY R,ESTAY D A S,MENG W,et al.A comparative risk analysis on CyberShip system with STPA-Sec,STRIDE and CORAS[J].Computers & Security,2023,128:103179.
[19]SADEGHI R,GOERLANDT F.A proposed validation frame-work for the system theoretic process analysis(STPA) technique[J].Safety Science,2023,162:106080.
[20]BENSACI C,ZENNIR Y,POMORSKI D,et al.STPA and Bowtie risk analysis study for centralized and hierarchical control architectures comparison[J].Alexandria Engineering Journal,2020,59(5):3799-3816.
[21]BENSACI C,ZENNIR Y,POMORSKI D,et al.Collision hazard modeling and analysis in a multi-mobile robots system transportation task with STPA and SPN[J].Reliability Engineering & System Safety,2023,234:109138.
[22]TSUJI M,TAKAI T,KAKIMOTO K,et al.Prioritizing scenarios based on STAMP/STPA using statistical model checking[C]//2020 IEEE International Conference on Software Testing,Verification and Validation Workshops(ICSTW).IEEE,2020:124-132.
[23]DE SOUZA F,DE MELO B J,HIRATA C M,et al.Combining STPA with SysML modeling[C]//2020 IEEE International Systems Conference(SysCon).IEEE,2020:1-8.
[24]ZHONG D,SUN R,GONG H,et al.System-theoretic processanalysis based on SysML/MARTE and NuSMV[J].Applied Sciences,2022,12(3):1671.
[25]DGHAYM D,HOANG T S,TURNOCK S R,et al.An STPA-based formal composition framework for trustworthy autonomous maritime systems[J].Safety Science,2021,136:105139.
[26]BEHRMANN G,DAVID A,LARSEN K G.A tutorial on uppaal[EB/OL].https://uppaal.org/texts/21-tutorial.pdf.
[27]LIU S,ZHOU C,SHAO H,et al.Research on automatic flight control system flight mode operation logic[C]//Journal of Phy-sics:Conference Series.2023.
[28]HÜBENER D,LUCKNER R,WEBER G.Concepts for Independent Monitoring of Flight Control Laws[C]//Proceedings of the 10th EUCASS-9th CEAS Aerospace Europe Conference 2023.2023.
[29]HANDBOOK A F.Federal Aviation Administration[R].Department of Transportation,1972.
[30]ISHIMATSU T,LEVESON N G,THOMAS J,et al.Modeling and Hazard Analysis Using STPA[C]//Proceedings of the 4th IAASS Conference.2010.
[31]MCCRACKEN D D,REILLY E D.Backus-naur form(BNF)[M]//Encyclopedia of Computer Science.2003:129-131.
[32]MAIDI M.The common fragment of CTL and LTL[C]//Proceedings of 41st Annual Symposium on Foundations of Compu-ter Science.IEEE,2000:643-652.
[1] ZHANG Cong, CHEN Zhe, WANG Huijie, WEI Yiyang. SCADE Model Checking Based on Implicit Predicate Abstraction and Property-directedReachability [J]. Computer Science, 2025, 52(12): 24-31.
[2] SHAO Wenxin, YANG Zhibin, LI Wei, ZHOU Yong. Natural Language Requirements Based Approach for Automatic Test Cases Generation of SCADE Models [J]. Computer Science, 2024, 51(7): 29-39.
[3] ZHENG Hong, QIAN Shihui, LIU Zerun, DU Wen. Formal Verification of Supply Chain Contract Based on Coloured Petri Nets [J]. Computer Science, 2023, 50(6A): 220300220-7.
[4] YANG Liu, FAN Hongyu, LI Dongfang, HE Fei. IC3 Hardware Verification Algorithm Based on Variable Hiding Abstraction [J]. Computer Science, 2023, 50(11A): 230200112-6.
[5] RAN Dan, CHEN Zhe, SUN Yi, YANG Zhi-bin. SCADE Model Checking Based on Program Transformation [J]. Computer Science, 2021, 48(12): 125-130.
[6] CAI Yong, QIAN Jun-yan, PAN Hai-yu. Approximate Safety Properties in Metric Linear Temporal Logic [J]. Computer Science, 2020, 47(10): 309-314.
[7] XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan. Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model [J]. Computer Science, 2019, 46(8): 206-211.
[8] HAN Ying-jie, ZHOU Qing-lei, ZHU Wei-jun. Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking [J]. Computer Science, 2019, 46(11): 25-31.
[9] ZHOU Nv-qi, ZHOU Yu. Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking [J]. Computer Science, 2018, 45(8): 288-294.
[10] LI Yun-chou,YIN Ping. Research of Model Checking Application on Aerospace TT&C Software [J]. Computer Science, 2018, 45(6A): 523-526.
[11] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure [J]. Computer Science, 2018, 45(4): 71-75.
[12] NIE Kai, ZHOU Qing-lei, ZHU Wei-jun and ZHANG Chao-yang. Modeling for Three Kinds of Network Attacks Based on Temporal Logic [J]. Computer Science, 2018, 45(2): 209-214.
[13] YANG Hong, HONG Mei, QU Yuan-yuan. Approach of Mutation Test Case Generation Based on Model Checking [J]. Computer Science, 2018, 45(11A): 488-493.
[14] ZHAO Ying, PAN Hua, ZHANG Yun-meng, MO Qi, DAI Fei. Modeling and Behavior Verification for Collaborative Business Processes [J]. Computer Science, 2018, 45(11A): 597-602.
[15] LIU Shuang, WEI Ou, GUO Zong-hao. Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm [J]. Computer Science, 2018, 45(10): 313-319.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.