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

2954 软件学报 2026 年第 37 卷第 7 期

车高速运动引发的多普勒效应和信号衰落, 保障信号传输过程中的稳定性与连续性面临诸多技术挑战 [2] . 此外, 高
速移动环境下的信道特性复杂多变, 易产生极端传输情形, 深度衰落、严重遮挡等因素会导致信号中断, 严重影响
通信的实时性和可靠性. 实际通信中, 无线信道测量难度大、成本高, 不仅依赖昂贵的设备支持, 也难以采集足量
的真实数据. 这使得高铁无线信道模型的正确性和可用性面临挑战. 准确、可靠的信道模型不仅能够模拟信道的
实际参数, 还能有效预测信道的衰落变化, 对于提高高铁无线通信的质量至关重要.
在构建无线通信信道模型时, 需充分考虑高铁的实际运行场景和信道的传播特性. 高铁的运行场景主要包括
高架桥、路堑、车站、丘陵地形和开放空间, 其中高架桥场景是最为典型且具有代表性的场景. 在高架桥场景中,
列车通常运行在无遮挡的开阔环境中. 尽管该场景下直射路径较为清晰, 但由于高架轨道的开阔性和信号的多径
反射, 会产生复杂的多径效应. 这种多径传播现象导致小尺度衰落和大尺度衰落效应并存, 从而形成了信道衰落的
特性 [3] . 信道衰落特性不仅造成信号强度不稳定, 还可能在关键时刻引发通信中断, 进而显著影响高铁通信的信道
容量和可靠性.
为有效描述这一信道衰落特性, 研究人员常基于小尺度衰落模型中的瑞利衰落信道和莱斯衰落信道建立高
铁无线通信信道模型. 例如, 冯业浩等人 [3] 结合实测数据和 Matlab 工具对高铁信道模型进行建模与分析, 基于莱
斯衰落模型提出了高铁信道的小尺度衰落模型. 王雪丽等人 [4] 针对高速铁路中的高架桥场景, 基于莱斯信道衰
落模型, 结合 LOS 直射分量推导了改进的信道估计公式. 相较于单一信道模型, 张逸康等人 [5] 提出了一种基于
瑞利衰落信道和莱斯衰落信道的复合信道模型, 通过理论推导得到了复合信道概率密度函数数学表达式. 在上
述研究中, 张逸康等人 [5] 聚焦于高架桥这一典型场景, 该场景下无线信道的建模和分析相对容易处理. 其提出的
复合信道概率密度函数结果完整, 具有普遍性与通用性. 复合信道模型中, 瑞利信道具有建模简单、计算便捷等
优点. 但上述研究工作均使用传统 Matlab 工具进行仿真验证, 可能因测量数据不准确或仿真算法不精确引入误
差和不确定性.
为确保无线通信信道模型的正确性和可靠性, 本文采用形式化方法, 通过其严格的数学证明和逻辑推理能力,
可以在理论上消除系统中的漏洞和安全缺陷, 在提高可靠性方面具有显著优势 [6] . 在应对复杂多样的无线信道建
模时, 形式化方法也展现出强大的潜力. 通过对信道的各种参数进行准确建模, 并借助定理证明工具验证信道模型
的正确性和关键性质, 形式化方法能够保障信道模型在各种条件下的可靠性 [7] . 这种方法有效满足了构建通用性
强且可靠性高的无线通信信道模型的需求, 为提升高铁无线通信的安全性和可靠性提供了重要的理论保障.
现阶段复合信道的形式化建模所需形式化数学理论研究现状如下: Mhamdi 等人 [8] 在定理证明器 HOL4 中提
出一种扩展实数的形式化, 并基于扩展实数进行了测度、积分等数学基础的形式化. 并且, Mhamdi 进一步在
[9]
HOL4 中完整地形式化数学基础, 并对信息论基础的核心概念进行了形式化建模. 但上述工作所形式化的数学基
础理论侧重于测度与 Lebesgue 积分, 对概率理论的内容形式化较少. 在信道的形式化相关研究中, Helali 等人 [10]
使用形式化方法, 从信道容量方面对级联信道进行了分析, 但其没有限定具体的信道模型. 本文基于以上工作, 在
定理证明器 HOL Light 中补充构建了数学基础与信息论基础, 用于复合信道的形式化建模.
本文参考张逸康等人 [5] 的建模方法, 针对高架桥场景, 采用形式化方法在 HOL Light 中对基于小尺度衰落模
型的高铁复合无线通信信道进行建模与验证. 针对复合信道的长尾分布特性, 本文运用定理证明技术, 验证了信道
模型中, 基站经高铁天线转发到用户手机的这一复合信道的概率密度函数符合第 2 类修正 Bessel 函数分布. 本文
主要贡献如下.
(1) 构建复合无线信道所需的扩展实数高阶逻辑定理库.
(2) 形式化定义复合无线信道所需的信息论基础概念.
(3) 形式化建立高架桥场景下的高铁复合无线通信信道模型并验证其概率密度函数性质.
本文第 1 节介绍高铁无线信道与建模基础形式化理论的相关工作. 第 2 节介绍定理证明器 HOL Light 和高铁
复合信道模型. 第 3 节介绍扩展实数数学基础形式化. 第 4 节介绍基于扩展实数的信息论基础形式化. 第 5 节介绍
高架桥场景下高铁复合无线通信信道的形式化建模与验证. 第 6 节总结全文.