Page 270 - 《软件学报》2026年第7期

买宁 等: 高铁复合无线通信信道形式化建模与验证 2955

1 相关工作

1.1 高铁无线信道研究现状
高速铁路正迈入无线通信的新时代, 随着 5G、6G 等技术的快速发展, 欧盟提出的“Shift2Rail”计划正推动高
铁从有线通信向无线通信的转变 [11] . 为推动未来高速铁路通信的可持续发展, 构建高速铁路无线通信的理论框架
至关重要, 而可靠的信道模型则是建立这一框架的基础.
近年来, 针对高铁通信信道建模的研究取得了一定进展. Zhou 等人 [12] 系统总结了先进的高铁信道建模方法,
从统计建模、理论建模等方面对高铁信道模型进行了介绍. Zhao 等人 [13] 针对城市、路堑和高架桥 3 种高铁通信
典型场景, 进行了全面的信道模型评估. 在高架桥这一场景中, 由于环境开阔等多种因素的影响, 衰落效应显著. Lin
等人 [14] 针对小尺度衰落对高速铁路通信的影响, 重点研究了铃木衰落信道对高铁通信覆盖性能的影响. 同时, 针
对类似的开阔场景, 王雪丽等人 [4] 结合莱斯衰落信道和叠加训练信道估计方法, 提出一种改进的信道估计模型. 相
较于单一信道模型, 张逸康等人 [5] 提出基于瑞利衰落信道和莱斯衰落信道的复合高铁无线通信信道模型, 用于描
述高架桥场景下的无线通信系统. 该复合信道模型的推导完整, 且具有较高的通用性.
上述高铁信道建模的研究成果为进一步建模高铁复合无线通信信道及开展后续验证工作奠定了基础. 但这些工
作均使用传统研究方法, 如数据建模与系统仿真, 其可能引入误差和不确定性. 而形式化方法能够有效避免潜在错
误, 保障信道模型的正确性与可靠性. Ferrari 等人 [7] 调研并深入分析了形式化方法在铁路系统开发中的应用前景, 强
调形式化方法是推动铁路领域实现安全可靠技术进步的重要基础. 综上, 本文基于张逸康等人 [5] 的研究工作, 对高架
桥场景下的高铁复合无线通信信道模型进行了形式化建模, 并在此基础上验证该模型的正确性及其关键性质.
1.2 复合信道模型的形式化数学理论研究现状
高铁复合无线通信信道模型的形式化依赖于一系列数学基础概念, 包括测度与积分、概率以及信息论. 为确
保复合信道建模的准确性, 本文对相关数学基础进行了形式化. 近年来, 数学基础的形式化取得了显著进展.
Mhamdi 等人 [9] 在定理证明器 HOL4 中形式化了扩展实数, 并基于此形式化了测度、积分等数学基础. 并且, Mhamdi
等人 [15,16] 还在 HOL4 中基于扩展实数提出了 Lebesgue 积分的形式化, 该积分相比于普通积分适用于更广泛的场
景. Boldo 等人 [17,18] 在 Coq 中提出了对 σ 代数、测度、简单函数以及非负可测函数积分的形式化. 以上工作集中
于测度和 Lebesgue 积分的形式化, 而对概率理论的形式化研究相对较少.
在概率理论方面, Qasim [19] 在 HOL4 中提出正态随机变量相关概念的形式化, 并验证了其重要性质. 随后, 尹
晓娜等人 [20] 在 HOL Light 中对测度和概率理论进行了系统的形式化建模, 实现了重要概率分布及其分布性质定理
的形式化建模与高阶逻辑推导. 该研究为本文工作提供了较为完善的测度与概率理论基础. 但其主要基于实数域
展开, 并不适用于高铁无线通信中极端情况的建模和重要性质的验证. 因此, 本文在 HOL Light 中进一步基于扩展
实数域形式化建模了测度、积分与概率等基本数学概念, 补充了正态随机变量的相关定义, 为高铁复合无线通信
信道建模提供了坚实的数学基础.
在信息论基础方面, Mhamdi 等人 [8,9] 基于形式化的数学基础理论, 在 HOL4 中构建了信息论基础框架, 包括熵、
互信息和信道容量等核心概念. 在这一框架中, 下述工作进一步完善了信息论基础形式化理论体系. Liu 等人 [21,22]
进一步形式化了马尔可夫链等概念, 为描述信息传递过程中的状态转移提供了重要工具. 并且, Dunchev 等人 [23] 形
式化了数据处理等式和 Jensen 不等式, 用于验证信息论属性. 在应用层面, Helali 等人 [10] 使用形式化的信息论基础
定义对于级联信道的性质进行了分析. 本文基于上述工作, 形式化了信源与信道、熵与信息等信息论基础核心概
念. 同时, 针对高铁复合无线信道建模的需求, 本文对瑞利衰落信道和莱斯衰落信道进行了形式化, 为后续复合信
道建模提供形式化基础.

2 基础知识

2.1 HOL Light 定理证明器
HOL Light 是以简洁和轻量级的设计著称的定理证明器, 广泛用于形式化证明数学定理与辅助推理, 其具有