| 评审组： | 计算机与系统科学组 | | 项目名称： | 航天控制软件形式化规约智能推演与验证 |
| 提名单位： | 陕西省知识产权局 |
| 提名等级： | 一等奖 |
| 提名单位意见： | 我单位认真审阅了该项目提名书及附件材料，确认全部材料真实有效，并按照要求对该项目的基本情况进行了公示，公示期间无异议。
项目围绕航天控制软件形式化规约难定义、难获取和难验证的关键问题，建立了具有完全正则表达能力的形式化规约理论框架，提出了大语言模型赋能的自然语言需求与程序代码规约智能推演方法，构建了规约驱动的统一验证及分层分解验证方法，形成了贯通“规约定义—智能推演—规约验证”的航天控制软件可信保障理论、方法与工具体系。项目成果成功应用于我国探月工程三期月地高速再入返回飞行器等多款航天软件，为国家重大工程得顺利实施提供了有力的保障。团队获批省部级智能软件构造与质量保障学科技术中心，入选陕西省三秦英才特殊支持计划“创全国一流团队”及陕西省重点科技创新团队，对相关研究有引领和示范作用，对学科建设和经济社会发展有重要的指导作用。
根据《陕西省科学技术厅关于2026年度省科学技术奖提名工作的通知》，参照自然科学奖评定条件和评定标准，
|
| 项目简介： | 
|
| 客观评价： | 
|
| 代表性论文专著目录： | 
|
| 主要完成人情况： | - 姓名：田聪
排名：1
行政职务：科学研究院常务副院长
技术职称：教授
工作单位：西安电子科技大学
完成项目时所在单位：西安电子科技大学
对本项目主要学术贡献：对科学发现1、2、3有创造性贡献：在科学发现1中，证明了命题投影时序逻辑具备表达完全正则语言的能力，并通过给出命题投影时序逻辑的判定算法，解决了命题投影（区间）时序逻辑的判定难题（代表性论文专著2、3）；在科学发现2中，建立了大语言模型赋能的航天控制软件形式化规约智能推演方法，实现了从自然语言需求与程序代码到完全正则形式化规约的自动构（代表性论文专著4）；在科学发现3中，提出了面向复杂航天控制软件的分层分解形式化规约验证方法，将系统验证分解为系统规约、组件行为和代码实现三个层次，实现逐层确认（代表性论文专著5、6）。
- 姓名：段振华
排名：2
行政职务：无
技术职称：教授
工作单位：西安电子科技大学
完成项目时所在单位：西安电子科技大学
对本项目主要学术贡献：对科学发现1、3有创造性贡献：在科学发现1中，提出并建立了投影时序逻辑的模型理论和公理系统，解决了命题投影时序逻辑的判定性、复杂性和表达性问题（代表性论文专著1、2）；在科学发现3中，提出了集系统建模、规约描述与程序验证于一体的可执行逻辑语言，实现软件模型与形式化规约在统一逻辑框架下的表示（代表性论文专著5）。
- 姓名：文成
排名：3
行政职务：无
技术职称：讲师
工作单位：西安电子科技大学
完成项目时所在单位：西安电子科技大学
对本项目主要学术贡献：对科学发现2有创造性贡献：针对自然语言需求，提出了层次化语义分解形式化规约生成方法；针对软件代码，提出了程序结构引导与验证反馈驱动的形式化规约推演框架（代表性论文专著4）。
- 姓名：王文胜
排名：4
行政职务：无
技术职称：讲师
工作单位：西安电子科技大学
完成项目时所在单位：西安电子科技大学
对本项目主要学术贡献：对科学发现1有创造性贡献：突破了无穷字自动机的确定化复杂性问题，提出了Streett自动机确定化的最优数据结构，改进了Emerson-Lei自动机的确定化算法，提升了完全正则规约的验证效率（代表性论文专著3）。
- 姓名：苏杰
排名：5
行政职务：无
技术职称：助理研究员
工作单位：西安电子科技大学
完成项目时所在单位：西安电子科技大学
对本项目主要学术贡献：对科学发现3有创造性贡献：提出了条件插值与动态偏序约简新方法，显著降低了形式化规约推演验证所需的时空开销，提高了有限资源下的验证规模和效率（代表性论文专著6）。
- 姓名：于斌
排名：6
行政职务：无
技术职称：副教授
工作单位：西安电子科技大学
完成项目时所在单位：西安电子科技大学
对本项目主要学术贡献：对科学发现3有创造性贡献：提出了统一执行、动静结合、并行验证的高效精确规约验证方法。（代表性论文专著5）。
|
| 主要完成单位： | - 单位名称：西安电子科技大学
单位贡献：项目围绕航天控制软件形式化规约难定义、难获取和难验证的关键问题，建立了具有完全正则表达能力的形式化规约理论框架，提出了大语言模型赋能的自然语言需求与程序代码规约智能推演方法，构建了规约驱动的统一验证及分层分解验证方法，形成了贯通“规约定义—智能推演—规约验证”的航天控制软件可信保障理论、方法与工具体系。项目成果成功应用于我国探月工程三期月地高速再入返回飞行器等多款航天软件，为国家重大工程得顺利实施提供了有力的保障。
西安电子科技大学作为本项目第一完成单位，全面负责项目的总体规划、设计、实施与组织，为本项目提供了大力支持和充分保障，确保了项目的顺利进行。
|
| 完成人合作关系说明： | 完成人合作关系说明：1
|
