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

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

密度函数符合第 2 类修正 Bessel 函数的分布. 在建模过程中, 本文在高阶逻辑定理证明器 HOL Light 中构建了扩
展实数基础与信息论基础, 为复合信道建模提供了坚实的理论支撑. 这一工作为高铁通信信道的形式化建模与验
证提供了可靠的理论指导, 也为后续其他复杂通信场景下的信道模型形式化建模与验证提供了通用的形式化建模
框架, 探索了实际通信场景形式化验证的可能性.

References
[1] Zhong ZD, Guan K, Chen W, Ai B. Challenges and perspective of new generation of railway mobile communications. ZTE Technology
Journal, 2021, 27(4): 44–50 (in Chinese with English abstract). [doi: 10.12142/ZTETJ.202104009]
[2] Wang YF. Application of high speed railway signal system based on wireless communication technology. Smart City Application, 2019,
2(1): 29–31 (in Chinese with English abstract). [doi: 10.33142/sca.v2i1.130]
[3] Feng YH, Zheng M, Bu ZY. Modelling and simulating radio channel in high-speed rail environment. Computer Applications and
Software, 2013, 30(3): 96–99, 169 (in Chinese with English abstract). [doi: 10.3969/j.issn.1000-386x.2013.03.026]
[4] Wang XL Wang HQ, Li X, Yang DK. Channel estimation method for massive MIMO system in rice channel. Telecommunications
Science, 2017, 33(9): 10–19 (in Chinese with English abstract). [doi: 10.11959/j.issn.1000-0801.2017257]
[5] Zhang YK, Wang GP, Ye RY. Composite wireless channel characteristics for communication systems on viaducts of high-speed railway.
ZTE Technology Journal, 2021, 27(4): 30–35 (in Chinese with English abstract). [doi: 10.12142/ZTETJ.202104007]
[6] Hasan O, Tahar S. Formal verification methods. In: Khosrow-Pour M, ed. Encyclopedia of Information Science and Technology. 3rd ed.,
Hershey: IGI Global Scientific Publishing, 2015. 7162–7170. [doi: 10.4018/978-1-4666-5888-2.ch705]
[7] Ferrari A, Beek MHT. Formal methods in railways: A systematic mapping study. ACM Computing Surveys, 2022, 55(4): 69. [doi: 10.
1145/3520480]
[8] Mhamdi T, Hasan O, Tahar S. Formalization of entropy measures in HOL. In: Proc. of the 2nd Int’l Conf. on Interactive Theorem
Proving. Berg en Dal: Springer, 2011. 233–248. [doi: 10.1007/978-3-642-22863-6_18]
[9] Mhamdi T. Information-theoretic analysis using theorem proving [Ph.D. Thesis]. Montréal: Concordia University, 2012.
[10] Helali G, Hasan O, Tahar S. Formal analysis of information flow using min-entropy and belief min-entropy. In: Proc. of the 16th
Brazilian Symp. on Formal Methods: Foundations and Applications. Brasilia: Springer, 2013. 131–146. [doi: 10.1007/978-3-642-41071-
0_10]
[11] Hu FY, Ling Z, Liu TD, Li HL, Ai B. Wireless perception of high-speed railway communication: Challenges, framework, and future
directions. IEEE Wireless Communications, 2024, 31(4): 284–292. [doi: 10.1109/MWC.022.2200630]
[12] Zhou T, Li HY, Wang Y, Liu L, Tao C. Channel modeling for future high-speed railway communication systems: A survey. IEEE
Access, 2019, 7: 52818–52826. [doi: 10.1109/ACCESS.2019.2912408]
[13] Zhao YR, Wang XY, Wang GP, He RS, Zou YL, Zhao ZY. Channel estimation and throughput evaluation for 5G wireless
communication systems in various scenarios on high speed railways. China Communications, 2018, 15(4): 86–97. [doi: 10.1109/CC.2018.
8357743]
[14] Lin SH, Wang HY, Li WY, Wang JY. Coverage analysis for high-speed railway communications with narrow-strip-shaped cells over
Suzuki fading channels. Entropy, 2024, 26(8): 657. [doi: 10.3390/e26080657]
[15] Mhamdi T, Hasan O, Tahar S. Formalization of measure and Lebesgue integration over extended reals in HOL. Technical Report, MLX
TR11, Concordia University, 2011.
[16] Mhamdi T, Hasan O, Tahar S. Formalization of measure theory and Lebesgue integration for probabilistic analysis in HOL. ACM Trans.
on Embedded Computing Systems (TECS), 2013, 12(1): 13. [doi: 10.1145/2406336.2406349]
[17] Boldo S, Clément F, Faissole F, Martin V, Mayero M. A Coq formalization of Lebesgue integration of nonnegative functions. Journal of
Automated Reasoning, 2022, 66(2): 175–213. [doi: 10.1007/s10817-021-09612-0]
[18] Boldo S, Clément F, Martin V, Mayero M, Mouhcine H. A Coq formalization of Lebesgue induction principle and Tonelli’s theorem. In:
Proc. of the 25th Int’l Symp. on Formal Methods. Lübeck: Springer, 2023. 39–55. [doi: 10.1007/978-3-031-27481-7_4]
[19] Qasim M. Formalization of normal random variables [Ph.D. Thesis]. Montréal: Concordia University, 2016.
[20] Yin XN, Wang GH, Shi ZP, Guan Y, Zhang QY, Zhang JZ. High-order-logical modeling and verification of region coverage algorithm
with swarm robots. Journal of Chinese Computer Systems, 2022, 43(3): 475–482 (in Chinese with English abstract). [doi: 10.20009/j.cnki.
21-1106/TP.2021-0576]
[21] Liu LY, Hasan O, Tahar S. Formal reasoning about finite-state discrete-time Markov chains in HOL. Journal of Computer Science and
Technology, 2013, 28(2): 217–231. [doi: 10.1007/s11390-013-1324-6]