Journal of Systems Engineering and Electronics ›› 2019, Vol. 30 ›› Issue (5): 959-973.doi: 10.21629/JSEE.2019.05.13

• Systems Engineering • Previous Articles     Next Articles

Qualitative analysis for state/event fault trees using formal model checking

Quan JIANG1,2(), Chunling ZHU1,*(), Siqi WANG1()   

  1. 1 College of Aerospace Engineering, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
    2 China Academy of Electronics and Information Technology, Beijing 100083, China
  • Received:2018-09-10 Online:2019-10-08 Published:2019-10-09
  • Contact: Chunling ZHU E-mail:jiangquan@nuaa.edu.cn;clzh@nuaa.edu.cn;wangsq@nuaa.edu.cn
  • About author:JIANG Quan was born in 1981. She is a doctor candidate in Nanjing University of Aeronautics and Astronautics, majoring in man-machine and environmental engineering. Her main research interests are embedded system fault analysis, system safety analysis, and formal verification and validation. E-mail: jiangquan@nuaa.edu.cn|ZHU Chunling was born in 1968. She is a professor in Nanjing University of Aeronautics and Astronautics, and her research lies in the fields of aircraft environment control, aircraft icing and protection, airborne equipment cooling, with a particular focus on man-machine and environmental engineering. E-mail: clzh@nuaa.edu.cn|WANG Siqi was born in 1990. She graduated from Nanjing University of Aeronautics and Astronautics in 2016, majoring in software engineering. And now she works in Huawei Company, mainly responsible for the safety design and analysis of electronic products. Her research interests include system modeling, requirement verification, and formal model checking. E-mail: wangsq@nuaa.edu.cn
  • Supported by:
    the National Natural Science Foundation of China(11832012);This work was supported by the National Natural Science Foundation of China (11832012)

Abstract:

A state/event fault tree (SEFT) is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems. Such systems are ubiquitous in all areas of everyday life, and safety and reliability analyses are increasingly required for these systems. SEFTs combine elements from the traditional fault tree with elements from state-based techniques. In the context of the real-time safety-critical systems, SEFTs do not describe the time properties and important time-dependent system behaviors that can lead to system failures. Further, SEFTs lack the precise semantics required for formally modeling time behaviors. In this paper, we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata (TA), and use the model checker UPPAAL to verify system requirements' properties. The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems. Finally, we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.

Key words: state/event fault tree (SEFT), timed automata (TA), model transformation, safety analysis