系统工程与电子技术 ›› 2023, Vol. 45 ›› Issue (5): 1553-1569.doi: 10.12305/j.issn.1001-506X.2023.05.33
• 可靠性 • 上一篇
牛浩田1, 马存宝1,*, 韩佩2, 衣健民1
收稿日期:
2022-08-25
出版日期:
2023-04-21
发布日期:
2023-04-28
通讯作者:
马存宝
作者简介:
牛浩田(1989—), 男, 博士研究生, 主要研究方向为航电系统的任务安全性智能化分析与验证、民航规章知识图谱构建与应用Haotian NIU1, Cunbao MA1,*, Pei HAN2, Jianmin YI1
Received:
2022-08-25
Online:
2023-04-21
Published:
2023-04-28
Contact:
Cunbao MA
摘要:
针对航电系统任务安全性分析缺少仿真与验证手段问题, 提出了一种面向航电系统任务安全性的形式化建模与验证方法。首先, 基于时间自动机理论与民航规章建立标准运行条件下航电系统任务过程的形式化模型。随后, 将危险致因和安全约束分别以状态变迁的方式注入该模型, 建立航电系统任务安全性验证模型。最后, 通过遍历状态空间验证模型的活性、危险致因的可达性以及安全约束的充分性, 实现任务安全性分析结果的自动化验证。实验结果表明, 所提方法具有可行性和有效性, 能够为持续进行的航电系统任务安全性分析和设计提供模型基础, 确保分析结果的正确性和完整性。
中图分类号:
牛浩田, 马存宝, 韩佩, 衣健民. 面向航电系统任务安全性的形式化建模与验证[J]. 系统工程与电子技术, 2023, 45(5): 1553-1569.
Haotian NIU, Cunbao MA, Pei HAN, Jianmin YI. Formal modeling and verification for mission safety of avionics system[J]. Systems Engineering and Electronics, 2023, 45(5): 1553-1569.
表1
TCAS任务过程中的不安全控制行为"
编号 | 不安全控制行为 |
H1-Uca1 | 飞行员未正确(未成功)将任何与TCAS任务相关的机动意图向管制员及时报告(包括实施TCAS决断之后恢复管制服务的意图; 决定执行TCAS决断并偏离管制指令的意图; TCAS提供的决策建议等) |
H1-Uca2 | 紧急情况下, 飞行员未优先响应TCAS决策建议 |
H1-Uca3 | 飞行员未正确(成功)执行TCAS决策建议 |
H1-Uca4 | 管制员提供了不恰当的管制指令, 导致两架飞机违反安全间隔 |
H1-Uca5 | 管制员提供了正确的管制措施但未被正确执行, 致使两架飞机违反安全间隔 |
H1-Uca6 | 管制员未向选择执行TCAS决断的飞行员提供空中活动通报 |
H1-Uca7 | TCAS未及时/未正确/未成功向飞行员提供发出空中交通态势信息, 发出危险态势警告以及决策信息 |
表2
与人为因素相关的TCAS任务失败危险致因"
类型 | 危险致因 |
H1-Uca1-CF1 | 飞行员认定能够自行恢复航线,无需报告管制单位 |
H1-Uca1-CF2 | 飞行机组不熟悉管制程序(防撞程序) |
H1-Uca1-CF3 | 机长因事(吃饭、轮休等)分散精力或离开执勤位置,轮换的机长不熟悉应急程序 |
H1-Uca1-CF6 | 不同通信方式导致消息被忽略(飞行员以语音方式回复管制员由数据链通信电文方式发送的指令) |
H1-Uca1-CF7 | 管制员未持续守听指定频率,影响飞行员发出意图报告 |
H1-Uca1-CF8 | 飞机处于特殊状态(如放油阶段),无线电缄默之前未协调确定监听频率 |
H1-Uca2-CF9 | 管制员提供了管制指令,与TCAS决断互相冲突,干扰了飞行员最后机动决策过程 |
H1-Uca2-CF10 | 机长未明确其职责,即紧急情况下飞行员的决策权限高于管制员 |
H1-UCa2-CF11 | 飞行员未明确TCAS的优先级高于管制员(即紧急态势下机组应优先响应TCAS决策) |
H1-Uca3-CF12 | 飞行机组错误预估飞机机动性能 |
H1-Uca3-CF13 | 由于转机型等原因,飞行机组未熟练掌握防撞程序和动作 |
H1-Uca3-CF14 | 机组未打开并应用TCAS |
H1-Uca3-CF16 | 飞行员身体或心理原因(疲劳等)导致其任务执行能力降低 |
H1-Uca3-CF20 | 炫光、废气、降水、雾气霜影响飞行员视觉,导致飞行员未正确感知态势信息 |
H1-Uca4-CF23 | 飞行员和管制员建立联系时未提供必要安全信息,致使管制员未能全面掌握态势信息 |
H1-Uca3-CF24 | 飞行员通过指定点时未报告经过时间和高度,影响飞行员掌握态势信息 |
H1-Uca4-CF25 | 管制员不熟悉管制程序 |
H1-Uca4-CF26 | 管制员提供了飞行员无法执行的管制决策(垂直速度调整或水平速度调整超过飞机机动性能) |
H1-Uca4-CF27 | 管制员在飞行员报告无法执行管制指令时,未能提供正确的更改指令确保间隔 |
H1-Uca4-CF28 | 飞行员未将TCAS提供的交通信息通报管制员 |
H1-Uca3-CF30 | 管制员未持续监视雷达信息(由于用餐或其他原因离开执勤工位) |
H1-Uca4-CF29 | 雷达提供了错误的危险接近态势信息,使得管制员未能正确辨识 |
H1-Uca4-CF31 | 管制员由于身体或心理原因,导致其任务能力下降 |
H1-Uca4-CF32 | 管制区接受雷达服务的航空器数量超过能够安全处理的数量,造成管制员工作负担 |
H1-Uca4-CF34 | 当检测到高度信息未经证实的两架飞行器相互接近时,未说明高度信息未经证明 |
H1-Uca4-CF35 | 管制员未向偏离原既定航路的飞行员通报位置 |
H1-Uca4-CF36 | 航空器报告的位置信息和雷达指示的位置信息有显著差别时,管制员未向飞行员通报其位置 |
H1-Uca4-CF37 | 管制员提供改变高度层决策时未考虑已在该高度层巡航飞行的飞机(该机拥有更高的优先权) |
H1-Uca5-CF38 | 飞行员未听清管制许可时,未立即要求管制员澄清 |
H1-Uca5-CF39 | 飞行员未严格遵守管制指令,未依照管制员指定的高度层飞行 |
H1-Uca5-CF40 | 管制员未监听航空器驾驶员对管制的复述,未纠正错误的复述 |
H1-Uca5-CF41 | 管制员使用了飞行员不熟悉的管制术语 |
H1-Uca5-CF42 | 飞行员按照管制员对其他飞机的管制指令飞行 |
H1-Uca5-CF43 | 飞行员在管制频率上收到不真实管制指令时未向管制员核实,未向该频率上所有航空器通报 |
H1-Uca6-CF44 | 管制员不熟悉应急情况下的管制程序,对其职责不明确 |
H1-Uca6-CF48 | 管制员离开执勤工位,或未佩戴耳机进行持续守听,出现岗位无人值守情况 |
H1-Uca6-CF49 | 管制区容量增加导致管制员工作过度负担 |
H1-Uca6-CF50 | 管制员过度疲惫导致任务执行能力下降 |
表3
与设备因素相关的TCAS任务失败危险致因"
编号 | 危险致因 |
H1-Uca1-CF4 | 通信设备失效或故障,机组成员未持续监听应急频率 |
H1-Uca1-CF5 | 通信频率阻塞(发射机阻塞管制频率或飞行员选择不恰当的陆空通信联络频率) |
H1-Uca3-CF15 | TCAS决断指令造成飞机失速 |
H1-Uca3-CF17 | 操纵系统失效,导致飞行员无法正常操控飞机 |
H1-Uca3-CF18 | 驾驶舱及其设备致使驾驶员在执行职责时过分专注或疲劳,出现操作失误 |
H1-Uca3-CF19 | 空速指示器等仪表不能清晰地向飞行员提供态势信息 |
H1-Uca3-CF21 | 依赖于外部能源的仪表在能源失效时向飞行员提供了不可靠的信息 |
H1-Uca3-CF22 | 自动驾驶器断开未向飞行员提供与驾驶舱其他警告截然不同的信号,自动驾驶仪和导航设备交联 |
H1-Uca4-CF33 | 雷达或地面无线电设备失效导致管制员无法提供管制服务 |
H1-Uca6-CF45 | 雷达提供了错误的态势信息,或未提供态势信息(如设备失效等原因) |
H1-Uca6-CF46 | 通信设备故障或频率阻塞导致管制员和飞行员之间无法建立可靠的通信方式 |
H1-Uca6-CF47 | 无线电设备失效导致管制无法提供雷达服务 |
H1-Uca7-CF51 | 飞机未装备应答机,影响TCAS感知态势信息,TCAS未探测到周围存在碰撞威胁的飞机 |
H1-Uca7-CF52 | 高度报告设备未按照增量间隔向空中交通管制自动发送气压高度信息的询问 |
H1-Uca7-CF53 | TCAS避撞逻辑欠缺,不能应对日益复杂的空中交通态势 |
H1-Uca7-CF54 | 逻辑欠缺问题导致TCAS未有效评估周围威胁飞机,或无法提供有效的TA和RA咨询 |
H1-Uca7-CF55 | 飞机未装备ADS-B,或ADS-B设备不满足适航条件 |
H1-Uca7-CF56 | ADS-B设备未定期发送本机信息 |
H1-Uca7-CF57 | 电子助航设备未准确向飞行员提供位置信息 |
H1-Uca7-CF58 | TCAS设备性能不满足适航要求 |
H1-Uca7-CF59 | TCAS告警系统提供了不可靠的告警信息 |
H1-Uca7-CF60 | ADS-B设备故障导致未提供准备的态势信息 |
表4
基于STAMP/STPA分析出的控制行为及相应的UPPAAL通道"
控制行为描述 | UPPAAL通道 |
飞行机组将决定执行TCAS决断建议的意图报告管制员 | send1! & send1? |
飞行机组向管制员报告当前态势信息 | send2! & send2? |
飞行机组将航路恢复的意图报告管制员 | send3! & send3? |
飞行机组操控飞机与他机危险接近 | appear! & appear? |
飞行机组操控飞机恢复原航路 | turnback! & turnback? |
管制员拒绝飞行机组恢复原航路的意图 | reject! & reject? |
管制员处于离岗状态, 未对飞行机组报告进行回复 | noreply! & noreply? |
飞行机组操控飞机执行避撞机动 | operate! & operate? |
飞行机组操控飞机成功避免碰撞 | success! & success? |
飞行机组未成功操控飞机避免碰撞 | avoidfail! & avoidfail? |
飞行机组操控飞机进入TCAS的TA告警范围 | reachTA! & reachTA? |
飞行机组操控飞机进入TCAS的RA告警范围 | reachRA! & reachRA? |
飞行员恢复正常驾驶状态 | back! & back? |
TCAS失效 | TCASfail! & TCASfail? |
ADS-B系统失效 | ADSBfail! & ADSBfail? |
TCAS发出TA告警 | outputTA! & outputTA? |
TCAS发出RA告警 | outputRA! & outputRA? |
TCAS取消告警 | clear! & clear? |
飞行机组未执行避撞机动 | noavoid! & noavoid? |
表6
模型活性验证语句描述、语句功能描述以及验证结果"
性质验证语句 | 语句功能描述 | 验证结果 | 执行时间/s | 消耗空间/kB |
A[]not deadlock | 模型无死锁 | 满足 | 0.016 | 10 324 |
A<>ADSB. collectingdata or ADS. normal or ADSB. nooutput | ADSB模型功能正常 | 满足 | 0.001 | 10 432 |
A<>Controller. wait or Controller.mode1 or Controller.mode2 or Controller. Leavestation | 管制员模型功能正常 | 满足 | 0.015 | 10 440 |
A<>Pilot. keep or Pilot. receiveTCAS or Pilot.MisMessage1 or Pilot. receiveMES1 or Pilot. Judge or … or Pilot. return | 飞行员模型功能正常 | 满足 | 0.015 | 10 488 |
A<>TCAS. surveillance or TCAS. detecting or TCAS. computeCPA or … or TCAS. noinput | TCAS模型功能正常 | 满足 | 0.002 | 10 492 |
A<>Airplane. cruise or Airplane. TAarea or Airplane. RAarea or Airplane. Avoid or … or Airplane. resolved | 飞机模型功能正常 | 满足 | 0.016 | 10 432 |
E<>Airplane.intrude | 两机危险接近风险状态可达 | 满足 | 0.001 | 10 492 |
表8
安全约束充分性验证语句描述、语句功能描述以及验证结果"
性质验证语句 | 语句功能描述 | 验证结果 | 执行时间/s | 消耗空间/kB |
A[]not (Airplane. misavoid or Airplane. stall or Airplane. failcommunication or Airplane. collisionarea or Pilot. wrongexecute or Pilot. missmessage2 or … or ADSB.outputwronginf) and (CA_1.withCA and CA_2 with CA and CA_3 withCA) and CA_4 withCA and CA_5 withCA and CA_6 withCA and CA_7 withCA | 在安全约束的限制下, 目标模型中所有危险状态均不可达 | 满足 | 98.125 | 1 278 540 |
1 | 肖刚. 飞机环境综合监视系统[M]. 上海: 上海交通大学出版社, 2019. |
XIAO G . Civil aircraft integrated surveillance system[M]. Shanghai: Shanghai Jiaotong University Press, 2019. | |
2 |
CHEN Y J , FENG W , JIANG Z Q , et al. An accident causation model based on safety information cognition and its application[J]. Reliability Engineering and System Safety, 2021, 207, 107363.
doi: 10.1016/j.ress.2020.107363 |
3 | 胡晓义, 王如平, 王鑫, 等. 基于模型的复杂系统安全性和可靠性分析技术发展综述[J]. 航空学报, 2020, 41 (6): 523436. |
HU X Y , WANG R P , WANG X , et al. Recent development of safety and reliability analysis technology for model-based complex system[J]. Acta Aeronautica et Astronautica Sinica, 2020, 41 (6): 523436. | |
4 |
DGHAYM D , HOANG T S , TURNOCK S R , et al. An STPA-based formal composition framework for trustworthy autonomous naritime systems[J]. Safety Science, 2021, 136, 105139.
doi: 10.1016/j.ssci.2020.105139 |
5 |
SHIN S M , LEE S H , SHIN S K , et al. STPA-based hazard and importance analysis on NPP safety I & C systems focusing on human-system interactions[J]. Reliability Engineering and System Safety, 2021, 213, 107698.
doi: 10.1016/j.ress.2021.107698 |
6 | ANDREWS J , TOLO S . Dynamic and dependent tree theory: a framework for the analysis of fault trees with dependent basic events[J]. Reliability Engineering & System Safety, 2022, 203, 108959. |
7 |
MAIO F D , BARALDI P , ESLAMIAN A . A dynamic event tree for a blowout accident in an oil deep-water well equipped with a managed pressure drilling condition monitoring and operation system[J]. Journal of Loss Prevention in the Process Industries, 2022, 79, 104834.
doi: 10.1016/j.jlp.2022.104834 |
8 | 石旭东, 成博源, 黄琨, 等. 基于模糊TOPSIS-FMEA的飞机IDG风险评价[J]. 系统工程与电子技术, 2022, 44 (6): 2060- 2064. |
SHI X D , CHENG B Y , HUANG K , et al. Risk assessment of aircraft IDG based fuzzy TOPSIS-FMEA[J]. Systems Engineering and Electronics, 2022, 44 (6): 2060- 2064. | |
9 |
NIU H T , MA C B , HAN P . A decentralized method for collision detection and avoidance applied to civil aircraft[J]. Proceedings of the Institution of Mechanical Engineers, Part G: Journal of Aerospace Engineering, 2021, 235 (6): 621- 645.
doi: 10.1177/0954410020953045 |
10 | Crashed during approach, Boeing 737-800, near Amsterdam Schiphol Airport[R]. Netherlands: The Dutch Safety Board, 2009: 46-50. |
11 | LEVESON N G . Rasmussen's legacy: a paradigm change in engineering for safety[J]. Applied Ergonomics, 2017, 59 (B): 581- 591. |
12 |
HU J Q , DONG S H , ZHANG L B , et al. Cyber-physical-social hazard analysis for LNG port terminal system based on interdependent network theory[J]. Safety Science, 2021, 137, 105180.
doi: 10.1016/j.ssci.2021.105180 |
13 |
牛浩田, 马存宝, 韩佩, 等. 民机气象雷达任务过程安全性分析方法研究[J]. 西北工业大学学报, 2020, 38 (1): 84- 94.
doi: 10.3969/j.issn.1000-2758.2020.01.011 |
NIU H T , MA C B , HAN P , et al. Study on safety analysis method to task process of civil aircraft weather radar system[J]. Journal of Northwestern Polytechnical University, 2020, 38 (1): 84- 94.
doi: 10.3969/j.issn.1000-2758.2020.01.011 |
|
14 | RISING J M , LEVESON N G . Systems-theoretic process analysis of space launch vehicle[J]. Journal of Space Safety Engineering, 2018, 5 (3): 153- 183. |
15 |
ZHOU X Y , LIU Z J , WANG F W , et al. A system-theoretic approach to safety and security co-analysis of autonomous ships[J]. Ocean Engineering, 2021, 222, 108569.
doi: 10.1016/j.oceaneng.2021.108569 |
16 | LI M , YAN F , NIU R , et al. Identification of causal scenarios and application of leading indicators in the interconnection mode of urban rail transit based on STPA[J]. Journal of Rail Transport Planning & Management, 2021, 17, 100238. |
17 |
CHAN C C , YANG C Z , FAN C F . Security verification for cyber-physical systems using model checking[J]. IEEE Access, 2021, 9, 75169- 75186.
doi: 10.1109/ACCESS.2021.3081587 |
18 |
QUAN J , ZHU C L , WANG S Q . Qualitative analysis for state/event fault trees using formal model checking[J]. Journal of Systems Engineering and Electronics, 2019, 30 (5): 959- 973.
doi: 10.21629/JSEE.2019.05.13 |
19 |
HAN X , TANG T , LV J . A hierarchical verification approach to verify complex safety control systems based on STAMP[J]. Science of Computer Programming, 2019, 172, 117- 134.
doi: 10.1016/j.scico.2018.11.006 |
20 | 钟德明, 宫浩原, 孙睿. 一种准确识别损失场景的STPA[J]. 北京航空航天大学学报, 2023, 49 (2): 311- 323. |
ZHONG D M , KONG H Y , SUN R . An STPA for accurately identifying loss scenarios[J]. Journal of Beijing University of Aeronautics and Astronautics, 2023, 49 (2): 311- 323. | |
21 | 肖国松, 刘嘉琛, 董磊, 等. 面向IMA通用系统管理的STPA安全性分析[J]. 中国安全科学学报, 2021, 31 (9): 8- 14. |
XIAO G S , LIU J S , DONG L . STPA safety analysis on IMA generic system management[J]. China Safety Science Journal, 2021, 31 (9): 8- 14. | |
22 | ZHAO C , DONG L , LI H , et al. Safety assessment of the reconfigurable integrated modular avionics based on STPA[J]. International Journal of Aerospace Engineering, 2021, 8875972. |
23 | 刘嘉琛, 董磊, 赵长啸, 等. 基于形式化方法的DIMA动态重构仿真与验证[J]. 系统工程与电子技术, 2022, 44 (4): 1282- 1290. |
LIU J C , DONG L , ZHAO C X , et al. Simulation and verification of DIMA dynamic reconfiguration based on formal method[J]. Systems Engineering and Electronics, 2022, 44 (4): 1282- 1290. | |
24 |
DAKWAT A L , VILLANI E . System safety assessment based on STPA and model checking[J]. Safety Science, 2018, 109, 130- 143.
doi: 10.1016/j.ssci.2018.05.009 |
25 |
SCARINCI A , QUILICI A , RIBEIRO D , et al. Requirement generation for highly integrated aircraft systems through STPA: an application[J]. Journal of Aerospace Information Systems, 2019, 16 (1): 9- 21.
doi: 10.2514/1.I010602 |
26 |
CHEN Y J , XU J H , KAN L J , et al. Equipment mission safety evaluation method based on function-structure[J]. IEEE Access, 2021, 9, 71356- 71371.
doi: 10.1109/ACCESS.2021.3078813 |
27 |
SULTANA S , OKOH P , HAUGEN S , et al. Hazard analysis: application of STPA to ship-to-ship transfer of LNG[J]. Journal of Loss Prevention in the Process Industries, 2019, 60, 241- 252.
doi: 10.1016/j.jlp.2019.04.005 |
28 | 刘传会, 张广泉. 一种基于时间自动机网络的实时系统形式化验证方法[J]. 苏州大学学报(自然科学版), 2008, (1): 35- 40. |
LIU C H , ZHANG G Q . A form verification method for real-time system based on networks of timed automata[J]. Journal of Suzhou University(Natural Science Edition), 2008, (1): 35- 40. | |
29 |
STROEVE S H , BLOM H A P , DROZDOWSKI S . Modeling and simulation of intrinsic uncertainties in validation of collision avoidance systems[J]. Journal of Air Transportation, 2020, 28 (4): 173- 183.
doi: 10.2514/1.D0187 |
30 |
NIU H T , MA C B , HAN P . Directional optimal reciprocal collision avoidance[J]. Robotics and Autonomous Systems, 2021, 136, 103705.
doi: 10.1016/j.robot.2020.103705 |
31 | PATRIARCA R , CHATZIMICHAILIDOU M , KARANIKAS N , et al. The past and present of system-theoretic accident model and processes and its associated techniques: a scoping review[J]. Safety Science, 2022, 146, 105566. |
32 | NIU H T , MA C B , HAN P , et al. A novel semantic cohesion approach for Chinese airworthiness regulations: theory and application[J]. IEEE Access, 2020, 8, 227729- 227750. |
[1] | 刘嘉琛, 董磊, 赵长啸, 陈泓兵. 基于形式化方法的DIMA动态重构仿真与验证[J]. 系统工程与电子技术, 2022, 44(4): 1282-1290. |
[2] | 周璇, 何锋, 谷晓燕, 贾子睿, 熊华钢. 航电系统体系贡献率权重演化动态综合评估[J]. 系统工程与电子技术, 2020, 42(8): 1740-1750. |
[3] | 范新峰, 谭志良. 基于数字对消的跟踪干扰抑制方法[J]. 系统工程与电子技术, 2020, 42(6): 1235-1240. |
[4] | 柯文俊, 陈静, 江山. 基于Petri网模型的系统仿真验证方法[J]. 系统工程与电子技术, 2017, 39(4): 924-930. |
[5] | 李友毅, 张志春, 熊壮, 肖景新, 李国辉. 舰载直升机着舰碰撞建模方法[J]. 系统工程与电子技术, 2015, 37(7): 1691-1696. |
[6] | 夏青元,徐锦法,张梁. 倾转旋翼飞行器无模型自适应姿态控制[J]. Journal of Systems Engineering and Electronics, 2013, 35(1): 146-151. |
[7] | 王亮, 康凤举, 邓红德, 陈怀民. 基于视觉的无人机着陆半物理仿真系统的应用[J]. Journal of Systems Engineering and Electronics, 2012, 34(7): 1511-1517. |
[8] | 杜湘瑜, 梁甸农. 分布式卫星SAR柔性仿真系统设计与实现[J]. Journal of Systems Engineering and Electronics, 2012, 34(5): 915-919. |
阅读次数 | ||||||
全文 |
|
|||||
摘要 |
|
|||||