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

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

reallim (atreal (&0) within {x | &0 <= x})
(\a. reallim at_posinfinity (\b. real_integral (real_interval [a, b])
(\v. &1 / v * exp (--v + --(power2 h / (&4 * power2 sigma1 * power2 sigma2 * v))))))
定理 6 证明了 p(h) 从公式 (9) 至公式 (10) 的化简与推导过程, 其关键证明步骤依赖于实数积分换元定理的实
∫ b ∫ g(b)
′
例化. 该定理规定了实数积分换元的条件与结果, 即 f(g(x))·g (x)dx = f(x)dx. 通过定理 6, p(h) 经过换元, 化
a g(a)
简为与公式 (10) 一致的结果. 此时结合公式 (7) 与 (10), 经过推导与验证, 可得出 p(h) 符合 K 0 分布这一结论, 即定
理 7.
定理 7. 换元结果符合 K 0 .
val it : thm =
⊢ sigma1 > &0 /\ sigma2 > &0
==> (&2 * h) / (power2 sigma1 * power2 sigma2) * Bessel_K0_real (abs h / (sigma1 * sigma2))
= h / (power2 sigma1 * power2 sigma2) *
reallim (atreal (&0) within {x | &0 <= x})
(\a. reallim at_posinfinity (\b. real_integral (real_interval [a, b]) (\v. &1 / v * exp (--v + --(power2 h / (&4 *
power2 sigma1 * power2 sigma2 * v))))))
至此, 通过定理 2–7 的逐步验证, 本文完成了定理 1 的形式化证明. 为进一步清晰定理 1 的证明过程, 公式 (11)
p(h) 的完整化简和换元推导过程. 其实质是将两条瑞利信道的统计特性综合起来, 建模用户最终接收到的
给出了
信号分布. 公式 (11) 的推导过程实际上反映了在高架桥这一高速移动场景下, 无线信号既受直接传输至用户的直
射衰落影响, 也受经车顶天线转发的多径衰落的综合影响, 复合信道共同决定高铁无线通信质量.

∫ ( ) ∫ ( )
 +∞ 1 h x 1 h

 p(h) = lim p h 1 , dh 1 + lim p h 1 , dh 1 , h 1 , 0


 x→0 +
 x |h 1 | h 1 x→0 − −∞ |h 1 | h 1






 ∫ h 2 h ∫ h 2 h
 +∞ h 2 x h 2
 1 1
 1 h 1 − − 1 h 1 − −
 2σ 2 h 1 2σ 2 h 2 2σ 2 h 1 2σ 2 h 2
2 1 dh 1 + lim
 = lim e 1 e e 1 e 2 1 dh 1

 2 2 2 2
 x→0 + x |h 1 | σ σ x→0 − −∞ |h 1 | σ σ

 1 2 1 2





 ∫ h 2 ∫ h 2
 +∞ h 2 x h 2
 1 h 1 − 1 h 1 −
 − 2σ 2 2σ 2 h 2 − 2σ 2 2σ 2 h 2
 2 1 dh 1 + lim
 = lim e 1 e 1 2 1 dh 1

 2 2 2 2
 x→0 + x |h 1 | σ σ x→0 − −∞ |h 1 | σ σ

 1 2 1 2





 ∫ h 2
 +∞ h 2
 1 h − 2σ 2 1 − 2σ 2 h 2
 = 2lim e 1 2 1 dh 1 (11)
 2 2
 x→0 + x h 1 σ σ

 1 2




 ∫
 2 +∞ 2
 h 1 σ h 2
 h −v−
 1 1 4σ 2 σ 2 v
令v = , p(h) = 2lim × e 1 2 dv


 2 2 2
 σ x→0 + x σ σ h 1 h 1
 1 1 2




 ∫ ∫
 +∞ 2 +∞
 h 2σ h 2 h h 2
 −v− 1 −v−
 1
1 2 dv =
1 2 dv
 = lim e 4σ 2 σ 2 v lim e 4σ 2 σ 2 v


 2 2 2 2 2
 σ σ x→0 + h σ σ x→0 + x v
 1 2 x 1 1 2




 ( )

 2h
 |h|

 = , h , 0
 K 0

2
σ σ 2 σ 1 σ 2
1 2
根据定理 1 可知, 在高架桥场景下, 复合信道概率密度函数在非零点处符合第 2 类修正 Bessel 函数 K 0 分布,
且具有连续性与可积性. 由其符合 K 0 分布, 可推出复合信道具有长尾特性, 该性质对无线通信系统设计与优化具
有重要意义.
6 总 结
本文针对高架桥场景下的高铁复合无线通信信道, 提出了一种基于小尺度衰落模型的复合信道的形式化建模
方法. 针对复合信道的长尾分布特性, 本文证明了基站信号经高铁车顶天线转发至用户终端这一复合信道的概率