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

doi:10.19665/j.issn1001-2400.2019.03.011

西安电子科技大学学报 ›› 2019, Vol. 46 ›› Issue (3): 66-73.doi: 10.19665/j.issn1001-2400.2019.03.011

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

丁明^1,²,张书玲¹,张琛³,张军²

^1. 西北大学信息科学与技术学院,陕西西安 710127
^2. 西安航空计算技术研究所,陕西西安 710119
^3. 西安电子科技大学计算机科学与技术学院,陕西西安 710071

收稿日期:2019-01-06 出版日期:2019-06-20 发布日期:2019-06-19
作者简介:丁明 (1982-),男,高级工程师,西北大学博士研究生,E-mail: dingmingdm@126.com.
基金资助:
国家自然科学基金(61502365);陕西省重点研发计划一般项目(2019GY-042)

Method for the verification of safety requirements of avionics systems

DING Ming^1,²,ZHANG Shuling¹,ZHANG Chen³,Zhang Jun²

^1. School of Information Science and Technology, Northwest University, Xi'an, 710127, China
^2. Xi'an Aeronautics Computing Technique Research Institute, AVIC, Xi'an, 710119, China
^3. School of Computer Science and Technology, Xidian University, Xi'an, 710071, China

Received:2019-01-06 Online:2019-06-20 Published:2019-06-19

摘要/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

中图分类号:

TP311

丁明,张书玲,张琛,张军. 一种航空电子系统安全性需求验证方法[J]. 西安电子科技大学学报, 2019, 46(3): 66-73.

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.

图/表 6

图1

图2

图3

图4

图5

图6

参考文献 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)

赞

可视化

摘要/Abstract

引用本文

使用本文

图/表 6

参考文献 15

相关文章 15

Metrics

本文评价

推荐阅读 10

[1]	沈利香,慕德俊,曹国,谢光前,束方勇. 针对硬件木马的形式化验证模型构造方法[J]. 西安电子科技大学学报, 2021, 48(3): 146-153.
[2]	舒新峰,王昌太,王燕,张丽丽. 一种命题投影时序逻辑的分布式模型检测方法[J]. 西安电子科技大学学报, 2020, 47(4): 39-47.
[3]	段钊, 刘锟龙. 采用CPAChecker的动态程序验证[J]. 西安电子科技大学学报, 2019, 46(1): 33-38.
[4]	李昊星;李凤华;宋承根;苏铓;刘歆. 支持多关键字的可搜索公钥加密方案[J]. J4, 2015, 42(5): 20-25.
[5]	逄涛;段振华;刘晓芳. Verilog程序的命题投影时序逻辑符号模型检测[J]. J4, 2014, 41(2): 79-84.
[6]	杨元原;马文平;刘维博;俞优;顾健. 带有异或运算安全协议的自动化检测[J]. J4, 2012, 39(4): 120-125+183.
[7]	李慧贤. 轻量级RFID双向认证协议设计与分析[J]. J4, 2012, 39(1): 172-178.
[8]	杨琛;段振华. 支持Stutter-不变性的命题区间时序逻辑[J]. J4, 2011, 38(2): 151-156.
[9]	金军;舒红平. 一种基于元胞自动机的安全多重图像水印算法[J]. J4, 2010, 37(1): 174-180.
[10]	邱钢;王宏;肖鸿;肖国镇. 两个前向安全盲签名体制的安全性分析[J]. J4, 2010, 37(1): 107-112+147.
[11]	杨潇潇;段振华. MSVL语言的公理系统的程序验证[J]. J4, 2010, 37(1): 96-101.
[12]	舒新峰;段振华. 投影时序逻辑的公理系统与形式验证[J]. J4, 2009, 36(4): 680-729.
[13]	张学军1;2;王东勇3;曾智勇2;尹忠海2. 一种新的具有附加特性的叛逆者追踪方案 [J]. J4, 2007, 34(2): 274-278.
[14]	司光东1;李艳平1;2;肖国镇1. 一种改进的群签名方案 [J]. J4, 2007, 34(1): 106-109.
[15]	辛向军(1;2);李发根(3);肖国镇(1). 对几种部分盲签名方案的安全性分析与改进 [J]. J4, 2006, 33(6): 953-955.