| 摘要: |
| 随着高铁无线通信质量需求日益增长, 高速移动场景下的通信可靠性已成为高铁无线通信中亟需关注和解决的核心问题. 构建可靠的信道模型是解决这一问题的关键. 高铁复合无线通信信道建模应充分考虑实际运行环境与信道传播特性, 以构建通用性强且可靠性高的无线通信信道模型. 在复杂无线信道建模方面, 形式化方法凭借其严谨的数学建模与严格的逻辑推理能力展现出显著优势. 在高架桥这一典型的高铁通信场景中, 结合形式化验证方法, 提出一种基于小尺度衰落模型的复合无线通信信道的高阶逻辑模型. 针对复合信道的长尾分布特性, 运用定理证明技术验证了复合无线通信信道的概率密度函数符合第2类修正Bessel函数的分布. |
| 关键词: 形式化方法 高铁无线通信 复合信道建模 定理证明 |
| DOI:10.13328/j.cnki.jos.007501 |
| 分类号:TP311 |
| 基金项目:国家自然科学基金(62272323, 62272322, 62372312) |
|
| Formalization and Verification of Composite Wireless Communication Channels in High-speed Railway |
|
MAI Ning1, GUAN Yong1, CHEN Shan-Yan1, WANG Guo-Hui1, LI Xi-Meng1, SHI Zhi-Ping1,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 |