这篇论文提出了一种新的空中交通管制程序运行时监控框架，通过结合无线电通信、监视数据和机载观察，能够有效识别程序偏差，对于提高空中交通安全具有重要意义。与传统的监控方法相比，该方法在真实交通和合成情况下的表现都十分出色，值得深入研究。
提出一个运行时验证框架，通过检查空中交通管制员与飞行员之间的交流、监视数据和机载观察来监控空中交通管制程序。该框架将无线电通信解析为与相关实体相关的事件，并将它们与监视和机载观察合并成一个时间戳记录。使用ICAO规定的义务作为时间公式进行评估。在真实交通中，该管道达到0.85的F1分数，在1,495个由两个公共语料库生成的合成情况下，监控逻辑在所有情况下都返回预期的判决。在两个由官方调查报告重建的历史事故中，监控器识别出调查人员记录的程序偏差。
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.