（通讯员 王小兵 常瀚堃）日前，第40届ASE2025（IEEE/ACM International Conference on Automated Software Engineering）国际学术会议在韩国首尔召开，ASE是国际软件工程领域的顶级学术会议，与ICSE、FSE并列为ACM SIGSOFT旗舰系列会议。西电tyc33455cc田聪教授团队的工作“Bridging Natural Language and Formal Specification-Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs”获得IEEE/ACM SIGSOFT Distinguished Paper Award杰出论文奖，也是公司首次获得该项殊荣。该奖项是国际软件工程领域最具影响力的学术荣誉之一，用以表彰在理论创新与工程实践方面均有突出贡献的研究工作。本次论文由田聪教授担任通讯作者，杨孟飞院士为指导专家，论文第一作者为青年教师马智，其余作者依次为文成、苏哲欣、梁潇和秦胜潮教授。
图1. IEEE/ACM SIGSOFT Distinguished Paper Award杰出论文奖
围绕形式规约难以提取的关键科学问题，该论文提出了创新性的层次化语义分解与大语言模型协同推理框架Req2LTL，通过引入一种分层中间表示OnionL（洋葱语言），将自然语言需求结构化解构为作用域、逻辑关系与原子命题的树形语义结构，并结合大模型的局部语义理解能力与确定性规则合成机制，实现语法正确的LTL自动生成。Req2LTL可以对复杂软件系统的需求进行智能理解和分析，并自动生成线性时序逻辑LTL形式规约，从而更好地保障系统的安全可信，解决了领域工程师理解和书写逻辑规约难的问题。
图2.马智博士在ASE2025会场进行现场报告
该科研工作围绕杨孟飞院士主持的国家自然科学基金重大项目《嵌入式软件智能合成基础理论与方法》所提出的关键科学问题展开。目前，Req2LTL工具已实际应用至我国重大航天工程，并且正在扩展至轨道交通、智能汽车、工控系统和操作系统等领域。马智博士在ASE2025会场现场报告了该科研工作，引起了热烈的反响与讨论，该工作为形式化方法在航天重大工程中的应用进行了初步探索，是推动其从理论研究走向工程实践的一次积极探索。
图3. ASE2025杰出论文颁奖仪式
