Page 72 - 《软件学报》2025年第12期

李春奕 等: 基于时序逻辑的需求文本隐含语义解析与推理 5453

表 10 模型在跨领域软件需求文档上的准确性评估

数据集 需求文本数量 Loss Precision Accuracy
太阳搜索控制需求 79 0.006 849 0.962 962 1.0
ARSC 795 0.201 903 0.912 500 0.796 296
自动驾驶需求 74 0.054 785 0.791 666 0.944 444

5 总 结

本文介绍了一种从自然语言需求文本中识别时序逻辑语义的方法 FSLNets-TLSA, 该方法对需求文本进行预
处理, 包括 POS 标记、数据降噪、依存分析以及文本向量化等步骤, 并使用小样本网络识别文本隐含的时序逻辑
语义, 同时为了应对更复杂的监控语义, 使用了 EDA 数据增强和 PGD 对抗训练两个方法, 提高了对复杂监控语义
的识别准确度. 在后续的工作当中, 将考虑将本文方法与现有的转换工具自动结合, 有望有效地处理自然语言中的
隐含时序语义, 从而改进整个自然语言转换为形式逻辑的流程和提高生成形式化规约的质量.

References:
[1] Pnueli A. The temporal logic of programs. In: Proc. of the 18th Annual Symp. on Foundations of Computer Science. Providence: IEEE,
1977. 46–57. [doi: 10.1109/SFCS.1977.32]
[2] Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In: Logic of Programs.
Yorktown Heights: Springer, 1982. 52–71. [doi: 10.1007/BFB0025774]
[3] Duan ZH, Tian C, Zhang L. A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica,
2008, 45(1): 43–78. [doi: 10.1007/S00236-007-0062-Z]
[4] Chen M, Tam Q, Livingston SC, Pavone M. Signal temporal logic meets reachability: Connections and applications. In: Proc. of the 13th
Workshop on the Algorithmic Foundations of Robotics. Cham: Springer, 2020. 581–601. [doi: 10.1007/978-3-030-44051-0_34]
[5] Tolmach P, Li Y, Lin SW, Liu Y, Li ZX. A survey of smart contract formal specification and verification. ACM Computing Surveys,
2022, 54(7): 148. [doi: 10.1145/3464421]
[6] Niang M, Riera B, Philippot A, Zaytoon J, Gellot F, Coupat R. A methodology for automatic generation, formal verification and
implementation of safe PLC programs for power supply equipment of the electric lines of railway control systems. Computers in Industry,
2020, 123: 103328. [doi: 10.1016/J.COMPIND.2020.103328]
[7] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1): 33–61 (in
Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm [doi: 10.13328/j.cnki.jos.005652]
[8] Bonnah E, Hoque KA. Runtime monitoring of time window temporal logic. IEEE Robotics and Automation Letters, 2022, 7(3):
5888–5895. [doi: 10.1109/lra.2022.3160592]
[9] Srinivasan M, Coogan S. Control of mobile robots using barrier functions under temporal logic specifications. IEEE Trans. on Robotics,
2021, 37(2): 363–374. [doi: 10.1109/TRO.2020.3031254]
[10] Zhou XY, Yang TG, Zou YY, Li SY, Fang H. Multiple subformulae cooperative control for multiagent systems under conflicting signal
temporal logic tasks. IEEE Trans. on Industrial Electronics, 2023, 70(9): 9357–9367. [doi: 10.1109/TIE.2022.3215812]
[11] Bruel JM, Ebersold S, Galinier F, Mazzara M, Naumchev A, Meyer B. The role of formalism in system requirements. ACM Computing
Surveys, 2022, 54(5): 93. [doi: 10.1145/3448975]
[12] Zhang N, Yang MF, Gu B, Duan ZH, Tian C. Verifying safety critical task scheduling systems in PPTL axiom system. Journal of
Combinatorial Optimization, 2016, 31(2): 577–603. [doi: 10.1007/S10878-014-9776-3]
[13] Wang XB, Guo WX, Zhao L, Shu XF. Runtime verification method for social network security based on source code instrumentation. In:
Proc. of the 8th Int’l Workshop on Structured Object-oriented Formal Language and Method. Gold Coast: Springer, 2018. 55–70. [doi: 10.
1007/978-3-030-13651-2_4]
[14] Zhang N, Wang M, Duan ZH, Tian C. Verifying properties of MapReduce-based big data processing. IEEE Trans. on Reliability, 2022,
71(1): 321–338. [doi: 10.1109/TR.2020.2999441]
[15] Pakonen A, Pang C, Buzhinsky I, Vyatkin V. User-friendly formal specification languages—Conclusions drawn from industrial
experience on model checking. In: Proc. of the 21st IEEE IEEE Int’l Conf. on Emerging Technologies and Factory Automation. Berlin:
IEEE, 2016. 1–8. [doi: 10.1109/ETFA.2016.7733717]