一种航空电子系统安全性需求验证方法

doi:10.19665/j.issn1001-2400.2019.03.011

Abstract

Abstract:

To ensure the correctness of avionics systems safety assessment, a model-based system safety requirements description and verification approach is proposed. First, hazard use cases are established and safety requirements are captured according to the system functional requirements, safety objectives and failure states. Second, the state machine diagrams with functional failure are used to describe the system functional model including safety requirements. The safety extended hierarchical automata are used as the intermediate models, and the formal description of the system functional model is realized by the transformation algorithm. Finally, the correctness of safety requirements is verified by model checking. Case studies are presented to show that this method can verify whether the designed system's functions meet the safety attributes and improve the accuracy and efficiency of safety assessment.

Key words: avionics systems, safety, formal methods, model checking

CLC Number:

TP311

DING Ming,ZHANG Shuling,ZHANG Chen,Zhang Jun. Method for the verification of safety requirements of avionics systems[J].Journal of Xidian University, 2019, 46(3): 66-73.

Figures/Tables 6

References 15

[1]	WANG H L, ZHAO T D, REN F C , et al. Integrated Modular Avionics System Safety Analysis Based on Model Checking [C]//Proceedings of the Annual Reliability and Maintainability Symposium. Piscataway: IEEE, 2017: 7889773.
[2]	SOCIETY OF AUTOMOTIVE ENGINEERS. Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment: ARP4761[S]. Warrendale: Society of Automotive Engineers, 1996.
[3]	EUGENE B, VYACHESLAV K, KOSTIANTYN L , et al. Reliability Assessment of Safety Critical System Considering Different Communication Architectures [C]//Proceedings of the 2018 IEEE 9th International Conference on Dependable Systems, Services and Technologies. Piscataway: IEEE, 2018: 17-20.
[4]	BITTNER B, BOZZANO M, CAVADA R , et al. The xSAP Safety Analysis Platform [C]// Lecture Notes in Computer Science: 9636. Heidelberg: Springer Verlag, 2016: 533-539.
[5]	NARY S, JANUSZ Z . Quantitative Assessment of Safety and Security of System Architectures for Cyberphysical Systems Using the NFR Approach[J]. IEEE Systems Journal, 2016,10(2):397-409. doi: 10.1109/JSYST.2013.2294628
[6]	MHENNI F, NGUYEN N, CHOLEY J Y . SafeSysE: A Safety Analysis Integration in Systems Engineering Approach[J]. IEEE Systems Journal, 2018,12(1):161-172. doi: 10.1109/JSYST.2016.2547460
[7]	PRIMA F, NIDI ANNISA R, LUSI S , et al. Safety Analysis at Weaving Department of PT. X Bogor Using Failure Mode and Effect Analysis (FMEA) and Fault Tree Analysis (FTA) [C]//Proceedings of the 2018 5th International Conference on Industrial Engineering and Applications. Piscataway: IEEE, 2018: 382-385.
[8]	YUTTHANA Y, TEERAWAT T . Reliability Modeling for Automatic Operation Mode of FSWO and FSWB System [C]//Proceedings of the 2017 3rd International Conference on Control, Automation and Robotics. Piscataway: IEEE, 2017: 487-490.
[9]	RAMBIKUR A, GIAMMARCO K , O'HALLORN B. Systems Architecture in Failure Analysis (Applications of Architecture Modeling to System Failure Analysis) [C]//Proceedings of the 2017 12th System of Systems Engineering Conference. Piscataway: IEEE, 2017: 7994966.
[10]	秦茂源, 慕德俊, 胡伟 , 等. 硬件安全门级细粒度形式化验证方法[J]. 西安电子科技大学学报, 2018,45(5):143-148.
	QIN Maoyuan, MU Dejun, HU Wei , et al. Fine-granularity Gate Level Formal Verification Method for Hard Ware Security[J]. Journal of Xidian University, 2018,45(5):143-148.
[11]	段钊, 刘锟龙 . 采用CPAChecker 的动态程序验证[J]. 西安电子科技大学学报, 2019,46(1):33-38.
	DUAN Zhao, LIU Kunlong . Dynamic Program Verification via a CPAChecker[J]. Journal of Xidian University, 2019,46(1):33-38.
[12]	MUHAMMAD W, MUHAMMAD USMAN S . Application of Model-based Systems Engineering in Small Satellite Conceptual Design-A Sysml Approach[J]. IEEE Aerospace and Electronic Systems Magazine, 2018,33(4):24-34.
[13]	SINDER G, OPDAHLO A L . Eliciting Security Requirements with Misuse Case[J]. Requirements Engineering, 2005,10(1):34-44. doi: 10.1007/s00766-004-0194-4
[14]	SEDAGHATBAF A, AZGOMI M A . Reliability Evaluation of UML/DAM Software Architectures under Parameter Uncertainty[J]. IET Software, 2018,12(3):236-244. doi: 10.1049/iet-sen.2017.0077
[15]	WEI Q X, JIAO J, Zhao T D . Flight Control System Failure Modeling and Verification Based on SPIN[J]. Engineering Failure Analysis, 2017,82:501-513. doi: 10.1016/j.engfailanal.2017.04.004

Method for the verification of safety requirements of avionics systems

RichHTML

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 6

References 15

Related Articles 15

Metrics

Comments

Recommended 10

[1]	SHEN Lixiang,MU Dejun,CAO Guo,XIE Guangqian,SHU Fangyong. Constructing formal verification models for hardware Trojans [J]. Journal of Xidian University, 2021, 48(3): 146-153.
[2]	SHU Xinfeng,WANG Changtai,WANG Yan,ZHANG Lili. Propositional projection temporal logic based distributed model checking method [J]. Journal of Xidian University, 2020, 47(4): 39-47.
[3]	WANG Yanfen,ZHU Xuran,YUN Xiao,SUN Yanjing,SHI Yunkai,WANG Sainan. Vehicle re-identification by multi-cameras for public security surveillance [J]. Journal of Xidian University, 2019, 46(4): 190-196.
[4]	DUAN Zhao, LIU Kunlong. Dynamic program verification via a CPAChecker [J]. Journal of Xidian University, 2019, 46(1): 33-38.
[5]	PANG Tao;DUAN Zhenhua;LIU Xiaofang. Symbolic model checking of Verilog programs with the propositional projection temporal logic [J]. J4, 2014, 41(2): 79-84.
[6]	YANG Yuanyuan;MA Wenping;LIU Weibo;YU You;GU Jian. Automatic detection of security protocols with XOR [J]. J4, 2012, 39(4): 120-125+183.
[7]	YANG Chen;DUAN Zhenhua. Stutter-invariant propositional interval temporal logic [J]. J4, 2011, 38(2): 151-156.
[8]	YANG Xiao-xiao;DUAN Zhen-hua. Verification of programs based on an axiom system for the MSVL language [J]. J4, 2010, 37(1): 96-101.
[9]	. Study of safety factors and non-probabilistic reliability measures of structures [J]. J4, 2009, 36(5): 916-920.
[10]	SHU Xin-feng;DUAN Zhen-hua. Axiomatization for the first-order projection temporal logic and formal verifications [J]. J4, 2009, 36(4): 680-729.
[11]	ZHANG Hai-bin;DUAN Zhen-hua. Model checking interval temporal logic [J]. J4, 2009, 36(2): 338-342.
[12]	ZHOU Hua;MENG Xiang-ru;ZHANG Li;QIAO Xiang-dong. Proactive recovery algorithm in the distributed intrusion-tolerance system [J]. J4, 2009, 36(2): 378-384.
[13]	ZHANG Hai-bin;DUANG Zhen-hua. Model checking multirate hybrid systems [J]. J4, 2008, 35(1): 60-648.
[14]	LIN Guo-qing;WANG Xin-mei. Reform of the Snort system by the multithreading technique [J]. J4, 2007, 34(6): 887-894.
[15]	GUO Jian1;JIN Nai-yong2. Vacuity detection in computation temperal logic [J]. J4, 2007, 34(5): 794-799.