Page 28 - 《软件学报》2025年第4期

1434 软件学报 2025 年第 36 卷第 4 期

[26] Ramesh Y, Rao MVP. Statistical model checking for probabilistic temporal epistemic logics. In: Proc. of the 14th Int’l Conf. on Agents
and Artificial Intelligence. Online: SciTePress, 2022. 53–63. [doi: 10.5220/0010847900003116]
[27] Zhu WJ, Wu HM, Deng ML. LTL model checking based on binary classification of machine learning. IEEE Access, 2019, 7:
135703–135719. [doi: 10.1109/ACCESS.2019.2942762]
[28] Jhala1 R, McMillan KL. Microarchitecture verification by compositional model checking. In: Proc. of the 13th Int’l Conf. on Computer
Aided Verification. Paris: Springer, 2001. 396–410. [doi: 10.1007/3-540-44585-4_40]
[29] McMillan KL. Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Proc. of the 11th
IFIP WG 10.5 Advanced Research Working Conf. on Correct Hardware Design and Verification Methods. Livingston: Springer, 2001.
179–195. [doi: 10.1007/3-540-44798-9_17]
[30] Namjoshi KS, Trefler RJ. Parameterized compositional model checking. In: Proc. of the 22nd Int’l Conf. on Tools and Algorithms for the
Construction and Analysis of Systems. Eindhoven: Springer, 2016. 589–606. [doi: 10.1007/978-3-662-49674-9_39]
[31] Zhou S, Wang JB, Xue PP, Wang XY, Kong L. An approach to the state explosion problem: SOPC case study. Electronics, 2023, 12(24):
4987. [doi: 10.3390/electronics12244987]
[32] Shen LX, Mu DJ, Cao G, Qin MY, Zhu JC, Hu W. Accelerating hardware security verification and vulnerability detection through state
space reduction. Computers & Security, 2021, 103: 102167. [doi: 10.1016/J.COSE.2020.102167]
[33] Jin Z. Environment Modeling-based Requirements Engineering for Software Intensive Systems. San Francisco: Morgan Kaufmann, 2018.
王小齐(1998－), 男, 硕士生, 主要研究领域为嵌
[doi: 10.1016/C2014-0-00030-5]
[34] Li WB, Hayes JH, Truszczyński M. Temporal action language (TAL): A controlled language for consistency checking of natural
language temporal requirements: (Preliminary results). In: Proc. of the 4th Int’l Symp. on NASA Formal Methods. Norfolk: Springer,
2012. 162–167. [doi: 10.1007/978-3-642-28891-3_16]

附中文参考文献:
[1] 杨孟飞, 顾斌, 段振华, 金芝, 詹乃军, 董云卫, 田聪, 李戈, 董晓刚, 李晓锋. 嵌入式软件智能合成框架及关键科学问题. 中国空间科
学技术, 2022, 42(4): 1–7. [doi: 10.16708/j.cnki.1000-758X.2022.0046]
[4] 黄友能, 张鹏基, 侯晓鹏, 唐涛. 基于混成自动机的城市轨道交通 ZC 子系统建模与验证方法. 中国铁道科学, 2016, 37(2): 114–121.
[doi: 10.3969/j.issn.1001-4632.2016.02.16]
[6] 杨璐, 陈永刚. 基于 MSC 与 UPPAAL 的区域控制器切换场景建模与验证. 铁道标准设计, 2018, 62(5): 171–174, 179. [doi:
10.13238/j.issn.1004-2954.201704260003]
[8] 李腾飞, 孙军峰, 吕新军, 陈祥, 刘静, 孙海英, 何积丰. 基于 SMT 的区域控制器同步反应式模型的形式化验证. 软件学报, 2023,
34(7): 3080–3098. http://www.jos.org.cn/1000-9825/6861.htm [doi: 10.13328/j.cnki.jos.006861]
[18] 刘筱珊, 袁正恒, 陈小红, 陈铭松, 刘静, 周庭梁. 区域控制器的安全需求建模与自动验证. 软件学报, 2020, 31(5): 1374–1391. http://
www.jos.org.cn/1000-9825/5952.htm [doi: 10.13328/j.cnki.jos.005952]

杨晓(2000－), 男, 硕士生, 主要研究领域为嵌入 陈小红(1982－), 女, 博士, 副教授, CCF 专业会
式软件需求验证, 形式化方法. 员, 主要研究领域为需求工程, 基于知识的软件
工程, 形式化方法.

金芝(1962－), 女, 博士, 教授, CCF 会士, 主要研
入式软件需求分析, 模型驱动开发. 究领域为软件需求工程, 知识工程.