发表机构
University of Genoa; CASD - University School of Advanced Defense Studies（热那亚大学; CASD - 高级国防研究大学学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出一种运行时验证框架，通过监控管制员与飞行员的口语交流、监视数据和机载观测，以形式化时序公式评估ICAO义务，能准确识别程序违规，在真实、合成场景及历史事故中均表现良好。
AI 中文摘要
空中交通管制程序通过管制员与飞行员之间的口语交流执行，这些交流对航空运输安全至关重要：执行过程中的失误可能引发严重运行危险，过往致命事故已证明了这一点。评估指令是否被遵循，需将所说内容与相关飞机、其状态以及飞行员必须履行的义务关联起来。本文提出一种运行时验证框架，通过监控管制员与飞行员的交流、监视数据和机载观测来对上述程序进行监控。该框架将无线电通信解析为与相关实体关联的事件，并将其与监视数据和机载观测合并为带时间戳的轨迹。源自国际民用航空组织（ICAO）的义务被形式化为带显式时间边界的时序公式，并在执行轨迹上进行评估。每次违规都会被报告，同时附带被违反的义务以及支持该裁决的观测结果。在真实交通场景中，完整流程针对盲注人类标注违规的F1值达到0.85；在从两个公开语料库衍生的1495种合成场景中，监控逻辑在所有情况下均返回预期裁决；在根据官方调查报告重建的两起历史事故中，该监控器识别出调查人员记录的相同程序偏差。
英文摘要
Air traffic control procedures are executed through spoken exchanges between controllers and pilots. These interactions are essential to the safety of air transportation: failures in their execution can create severe operational hazards, as evidenced by past fatal accidents. Assessing whether an instruction has been followed requires relating what was said to the aircraft concerned, its state, and the obligations that pilots must meet. We present a runtime verification framework that monitors such procedures by checking controller-pilot exchanges, surveillance data, and onboard observations. The framework parses radio communications into events linked to the entities they concern and merges them with surveillance and onboard observations into a time-stamped trace. The ICAO-derived obligations as formalized as temporal formulas with explicit time bounds and evaluated over execution traces. Every violation is reported along with the breached obligations and the observations that support the verdict. With real traffic, the complete pipeline reaches an F1 of 0.85 against blind human-annotated violations; in 1,495 synthetic situations derived from two public corpora, the monitor logic returns the expected verdict in every case. In two historical accidents reconstructed from official investigation reports, the monitor identifies the same procedural deviations documented by the investigators.
