用大模型形式化软件需求，提升需求可追溯性与验证效率
Working Document -- Formalising Software Requirements with Large Language Models
- 利用大语言模型自动提取和形式化软件需求
- 构建需求与代码间的可追溯链条，支持形式化验证
- 适合软件工程与形式化方法研究者参考
本文为工作文档，汇总了94篇相关论文，涵盖软件需求可追溯性（第4节）、形式化方法及其工具（第5节）、统一编程理论（UTP）与机构理论（第6节）。相比近期类似标题的投稿[7,8]，[7]为提交至爱尔兰ADAPT年度会议的两页摘要，于2025年3月18日提交，经轻量盲审后接受为海报展示，会议于2025年5月15日举行；[8]为提交至SAIV 2025的九页主文加九页参考文献与总结表格的长文，于2025年4月24日提交，经历严格评审。arXiv上传版本为根据评审意见改进后的优化版。
原文摘要 · Abstract (English)
This draft is a working document, having a summary of nighty-four (94) papers with additional sections on Traceability of Software Requirements (Section 4), Formal Methods and Its Tools (Section 5), Unifying Theories of Programming (UTP) and Theory of Institutions (Section 6). Please refer to abstract of [7,8]. Key difference of this draft from our recently anticipated ones with similar titles, i.e. AACS 2025 [7] and SAIV 2025 [8] is: [7] is a two page submission to ADAPT Annual Conference, Ireland. Submitted on 18th of March, 2025, it went through the light-weight blind review and accepted for poster presentation. Conference was held on 15th of May, 2025; [8] is a nine page paper with additional nine pages of references and summary tables, submitted to Symposium on AI Verification (SAIV 2025) on 24th of April, 2025. It went through rigorous review process. The uploaded version on arXiv.org [8] is the improved one of the submission, after addressing the specific suggestions to improve the paper.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。