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

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

通信系统中常见的信道模型. 本文根据高铁复合无线信道形式化的需要建模了一系列通用衰落信道, 包括传播路
径损耗信道、阴影衰落信道以及小尺度衰落模型中的莱斯衰落信道和瑞利衰落信道. 其中, 瑞利衰落信道的统计
特性能够较好地描述高架桥场景中无线信道的随机波动特征. 其信道模型简单, 具有良好的数学可处理性, 常用于
理论建模和性能分析. 瑞利衰落信道模型假设信号通过无线信道之后, 其信号幅度随机变化. 当主导传播路径非直
射路径时, 信号的衰落分布可用瑞利分布描述. 其概率密度函数如公式 (4) 所示.

r −r 2
f(r) = e 2σ 2 (4)
σ 2
此处重点介绍瑞利信道的形式化建模过程, 其建模思路与第 3.3 节中正态随机变量的形式化思路一致. 首先,
依据公式 (4) 形式化瑞利概率密度函数, 如定义 19 所示.
定义 19. Rayleigh 概率密度函数.
⊢ !r sigma. Rayleigh_loss_density r sigma =

r / power2 sigma * exp (--power2 r / (&2 * power2 sigma))
其次, 基于瑞利概率密度函数的形式化模型, 定义 20 所反映的瑞利概率测度被描述为定义 19 在 Lebesgue-
Borel 测度上的积分形式.
定义 20. Rayleigh 概率测度.
⊢ !sigma A. rayleigh_pmeasure sigma A =
(if A IN measurable_sets_ext lborel then pos_fn_integral lborel
(\x. extreal_mul (Normal (Rayleigh_loss_density (drop x) sigma)) (indicator_fn_ext A x))
else extreal_of_num 0)
最后, 以概率测度为基础形式化瑞利衰落信道, 通过验证随机变量的测度分布与 Rayleigh 概率测度一致表示
其满足 Rayleigh 分布特性. 瑞利衰落信道的形式化如定义 21 所示.
定义 21. Rayleigh 衰落信道.
⊢ !p X sigma. rayleigh_rv X p sigma <=>

random_variable_ext X p real_borel /\ measurable_distr p X = rayleigh_pmeasure sigma
瑞利衰落信道是复合无线信道形式化建模的基础, 当信道由两个或多个瑞利信道级联而成时, 信号分布将发
生改变, 不再是标准的瑞利分布.
5 高铁复合无线通信信道形式化建模与验证

高铁通信中, 高速移动、地形复杂和信号衰落等因素使信道建模变得困难. 而对信道进行形式化建模可以解
决实测数据难获取、成本高等问题, 同时能够准确建模信道特性, 为构建可靠的通信系统提供坚实的理论基础. 在
高架桥这一典型高铁通信场景中, 信号从基站直接至用户设备这一路径为第 2 条无线信道 h 1 , 基站发出信号经车
顶中继天线转发至用户设备为第 1 条无线信道 h 2 , 其信道模型如图 1 所示. 上述两条无线信道可建模为小尺度衰
落模型中的瑞利信道, 对应复合信道形式化模型如定义 22 所示, 即信号在复合信道中的分布模型与复合信道的概
率测度空间保持一致.
定义 22. 复合信道模型.
⊢ !p X sigma. product_rayleigh_rv X p sigma <=>
random_variable_ext X p real_borel /\ measurable_distr p X = product_rayleigh_pmeasure sigma
定义 22 中, “product_rayleigh_pmeasure”表示复合信道的概率测度, 其形式化建模依赖于复合信道的概率密度
函数. 依据文献 [5] 中给出的复合信道 h 的概率密度函数, h 表示信道 h 1 和 h 2 复合后的随机变量. 当衰减因子 c = 1

时, 复合信道的概率密度函数 p(h) 数学定义可由边缘分布与联合分布的关系简要表示为公式 (5). 衰减因子 c 反映
了信号转发过程中由于反射、散射、吸收所引入的额外衰减, 公式 (5) 表示信道经车顶中继转发至用户过程中,
不产生额外衰减时复合信道的概率密度函数.