Int J Performability Eng ›› 2020, Vol. 16 ›› Issue (2): 238-254.doi: 10.23940/ijpe.20.02.p8.238254

• Orginal Article • Previous Articles     Next Articles

Model-based Safety Analysis for an Aviation Software Specification

Jun Huac, Shuo Chenac*(), Defeng Chend, Jiexiang Kangb, and Hui Wangb   

  1. a College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, 211106, China
    bDepartment of Software, China National Aeronautic Radio Electronics Research Institute, Shanghai, 200233, China
    cCollaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing, 210007, China
    dSchool of Mechanical Engineering, Hefei University of Technology, Hefei, 230601, China
  • Submitted on ; Revised on ; Accepted on
  • Contact: Shuo Chen
  • About author:

    Hu Jun received his Ph.D. in computer software and theory from Nanjing University in 2006. He is an associate professor at Nanjing University of Aeronautics and Astronautics. His research interests include model-based safety analysis, software analysis, and formal methods.

    Chen Shuo is a master’s candidate at Nanjing University of Aeronautics and Astronautics. His research interests include software analysis and system safety analysis.

    Chen Defeng is a student at Hefei University of Technology. His research interests include machine learning and robot engineering.

    Kang Jiexiang is a researcher at China National Aeronautic Radio Electronics Research Institute. His research interests include avionics technology, software engineering, and embedded operating systems.

    Wang Hui is a senior engineer at China National Aeronautic Radio Electronics Research Institute. Her research interests include software engineering and software verification.

  • Supported by:
    The work was supported by the National Basic Research Program of China (973 Program) (No. 2014CB744903), the Foundation of Graduate Innovation Center in Nanjing University of Aeronautics and Astronautics (No. kfjj20181607), and “the Fundamental Research Funds for the Central Universities” (No. 61400020404).


Model-based safety analysis (MBSA) is a kind of safety analysis technology that combines system fault models with formal analysis methods. In this paper, a real flight guidance subsystem (FGS) in aviation domain is studied, and an example of safety modeling and formal analysis of high-level software requirement specification is given. A framework of model transformation is established, which can transform a high-level FGS software requirement model described by Requirement State Machine Language (RSML-e) into a formal NuSMV model. Then, according to the real system requirements and engineering experience, the relevant failure modes and the safety properties that need to be verified are designed. Finally, formal safety analysis and verification based on NuSMV are implemented in a platform xSAP. This case study shows that the MBSA method can be used effectively for the safety analysis of the real aviation system.

Key words: Flight guidance system, MBSA, NuSMV, xSAP, fault extension, fault tree, FMEA