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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2026,37(7):2953−2967 [doi: 10.13328/j.cnki.jos.007501] [CSTR: 32375.14.jos.007501] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
高铁复合无线通信信道形式化建模与验证

买 宁 1 , 关 永 1 , 陈善言 1 , 王国辉 1 , 李希萌 1 , 施智平 1,2

1
(首都师范大学 信息工程学院, 北京 100048)
2
(北京市科学技术研究院, 北京 100089)
通信作者: 王国辉, E-mail: ghwang@cnu.edu.cn

摘 要: 随着高铁无线通信质量需求日益增长, 高速移动场景下的通信可靠性已成为高铁无线通信中亟需关注和
解决的核心问题. 构建可靠的信道模型是解决这一问题的关键. 高铁复合无线通信信道建模应充分考虑实际运行
环境与信道传播特性, 以构建通用性强且可靠性高的无线通信信道模型. 在复杂无线信道建模方面, 形式化方法凭
借其严谨的数学建模与严格的逻辑推理能力展现出显著优势. 在高架桥这一典型的高铁通信场景中, 结合形式化
验证方法, 提出一种基于小尺度衰落模型的复合无线通信信道的高阶逻辑模型. 针对复合信道的长尾分布特性, 运
用定理证明技术验证了复合无线通信信道的概率密度函数符合第 2 类修正 Bessel 函数的分布.
关键词: 形式化方法; 高铁无线通信; 复合信道建模; 定理证明
中图法分类号: TP311

中文引用格式: 买宁, 关永, 陈善言, 王国辉, 李希萌, 施智平. 高铁复合无线通信信道形式化建模与验证. 软件学报, 2026, 37(7):
2953–2967. http://www.jos.org.cn/1000-9825/7501.htm
英文引用格式: Mai N, Guan Y, Chen SY, Wang GH, Li XM, Shi ZP. Formalization and Verification of Composite Wireless
Communication Channels in High-speed Railway. Ruan Jian Xue Bao/Journal of Software, 2026, 37(7): 2953–2967 (in Chinese). http://
www.jos.org.cn/1000-9825/7501.htm

Formalization and Verification of Composite Wireless Communication Channels in High-speed
Railway
1
1
1
1
1
MAI Ning , GUAN Yong , CHEN Shan-Yan , WANG Guo-Hui , LI Xi-Meng , SHI Zhi-Ping 1,2
1
(Information Engineering College, Capital Normal University, Beijing 100048, China)
2
(Beijing Academy of Science and Technology, Beijing 100089, China)
Abstract: With the growing demand for wireless communication quality in high-speed railway (HSR), ensuring communication reliability
in high-mobility scenarios has become a critical challenge. Constructing a reliable channel model is the key to addressing this issue. To
build a highly general and reliable channel model, composite wireless communication channel modeling requires full consideration of the
actual operating environment and channel propagation characteristics. With rigorous mathematical modeling and logical reasoning
capabilities, the formal method demonstrates significant advantages in complex wireless channel modeling. Focusing on the typical HSR
communication scenario of viaducts, this study proposes a high-order logic model of composite wireless communication channels based on
a small-scale fading model using the formal method. To address the long-tail characteristic of composite channels, the theorem proving
technique is used to verify that the probability density function (PDF) of the composite wireless communication channel conforms to the
distribution of the modified Bessel function of the second kind.
Key words: formal method; high-speed railway wireless communication; modeling of composite channels; theorem proving

随着京张高铁等智能化高铁的开通, 中国高铁正步入高质量发展的新阶段, 人们对高铁中无线通信质量的需
求也日益增长. 在高速移动场景中, 通信可靠性已成为高铁无线通信中亟需重点关注和解决的核心问题 [1] . 由于列

* 基金项目: 国家自然科学基金 (62272323, 62272322, 62372312)
收稿时间: 2024-12-28; 修改时间: 2025-03-17, 2025-04-30; 采用时间: 2025-06-30; jos 在线出版时间: 2025-11-20
CNKI 网络首发时间: 2025-11-21