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

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

[22] Liu LY, Hasan O, Aravantinos V, Tahar S. Formal reasoning about classified Markov chains in HOL. In: Proc. of the 4th Int’l Conf. on
Interactive Theorem Proving. Rennes: Springer, 2013. 295–310. [doi: 10.1007/978-3-642-39634-2_22]
[23] Dunchev C, Helali G, Hasan O, Tahar S. Formalization of DPI and Jensen’s inequality in HOL. Technical Report, DPI TR16, Concordia
University, 2016.

附中文参考文献
[1] 钟章队, 官科, 陈为, 艾渤. 铁路新一代移动通信的挑战与思考. 中兴通讯技术, 2021, 27(4): 44–50. [doi: 10.12142/ZTETJ.202104009]
[2] 王亚飞. 基于无线通信技术的高速铁路信号系统应用. 智能城市应用, 2019, 2(1): 29–31. [doi: 10.33142/sca.v2i1.130]
[3] 冯业浩, 郑敏, 卜智勇. 高速铁路环境下的无线信道建模与仿真. 计算机应用与软件, 2013, 30(3): 96–99, 169. [doi: 10.3969/j.issn.
1000-386x.2013.03.026]
[4] 王雪丽, 王海泉, 李肖, 杨大款. 莱斯衰落信道下大规模 MIMO 系统中的信道估计方法. 电信科学, 2017, 33(9): 10–19. [doi: 10.11959/
j.issn.1000-0801.2017257]
[5] 张逸康, 王公仆, 叶如意. 高速铁路高架桥场景中的复合无线信道特性. 中兴通讯技术, 2021, 27(4): 30–35. [doi: 10.12142/ZTETJ.
202104007]
[20] 尹晓娜, 王国辉, 施智平, 关永, 张倩颖, 张景芝. 群机器人区域覆盖算法高阶逻辑建模与验证. 小型微型计算机系统, 2022, 43(3):
475–482. [doi: 10.20009/j.cnki.21-1106/TP.2021-0576]

作者简介
买宁, 硕士, 主要研究领域为形式化验证, 高可靠嵌入式系统.
关永, 博士, 教授, 博士生导师, CCF 专业会员, 主要研究领域为形式化验证, 高可靠嵌入式系统.
陈善言, 博士, 主要研究领域为形式化验证, 高可靠嵌入式系统.
王国辉, 博士, 高级实验师, CCF 专业会员, 主要研究领域为形式化验证, 高可靠嵌入式系统.
李希萌, 博士, 副教授, CCF 专业会员, 主要研究领域为形式化方法, 软件验证.
施智平, 博士, 教授, 博士生导师, 主要研究领域为形式化验证, 视觉信息处理.