CCF软件大会2026|安全攸关软件的智能开发与验证论坛

二、论坛组织委员会

• 胡春明  教授 （北京航空航天大学）

• 詹乃军  教授 （北京大学）

• 金   芝  教授 （北京大学/武汉大学）

• 葛   宁  教授 （北京航空航天大学）

三、论坛安排

日程安排：

时间：2026年11月8日，09:00~12:00

地点：天津市社会山国际会议中心酒店  三层接见厅

论坛议程：

四、论坛报告嘉宾简介

1. 报告人：程胜 研究员

题目：载人航天工程软件智能化独立审查：工程需求、关键技术与应用探索

摘要：载人航天工程软件的高安全性与高可靠性要求，对独立审查的覆盖范围、分析深度和证据充分性提出了严苛要求。本报告围绕需求与代码实现一致性确认、设计与代码一致性验证、常见及多发软件故障模式检查、静态分析告警中的误报筛选确认四项核心任务，阐述智能化独立审查的工程需求与技术路径。重点介绍领域知识图谱构建、需求与设计要素治理及建模、代码语义理解、需求—设计—代码—测试双向追溯，以及软件故障模式表征与识别等关键技术，介绍自主开发的软件智能审查智能体及其在载人运载火箭飞行控制软件中的初步应用。应用结果表明，该方法在审查效率、分析深度与覆盖广度方面取得显著提升。最后，讨论智能审查结果的可信性、证据可追溯性与人机协同复核机制，为安全攸关软件智能化开发与验证提供工程参考。

简介：程胜，博士，研究员，国务院特殊津贴专家，中国航天科技集团学术带头人、科技创新团队负责人。担任中国载人航天工程软件工程和数字化技术发展和管理中心主任，中国载人航天工程软件专家组副组长、数字化专家组副组长，中国航天科技集团科技委软件专业组副组长。主要从事航天装备基础软件、智能软件工程等技术研究。主持过国家核高基重大专项、国家重点研发计划、载人航天软件专项等二十多项国家级重大软件项目研发。主持研发的航天装备高可靠实时操作系统、软件开发环境、智能故障诊断系统等成果已应用于我国新一代卫星、运载火箭等重大型号以及载人航天等重大航天工程，是支撑航天装备信息化和智能化的重要配套软件产品。

2. 报告人：武方方 研究员

题目：安全攸关软件模型驱动研发中的AI与形式化方法

摘要：以安全攸关软件的模型驱动研发为背景，介绍AI辅助需求建模、架构与行为模型生成的探索。结合形式化分析与仿真验证，阐述AI与形式化方法的结合方式，讨论需求语义保持、模型一致性及生成结果检查中的典型问题与处理方法。

简介：武方方，研究员，中航工业自控所副总师，工学博士。从事飞行控制嵌入式系统及软件开发测试工作近20年，熟练掌握嵌入式系统设计、软件开发与验证技术。在C919项目飞控电子包软件研发过程中与霍尼韦尔（Honeywell）开展深入合作，具有基于模型的系统工程（MBSE）在嵌入式计算机系统研制中的工程实践经验。

3. 报告人：卜磊 教授 

题目：面向人机物融合场景的软件可信构造与保障

摘要：人机物融合系统广泛出现在列控、航天、航空、智能驾驶等安全攸关领域，其行为正确性至关重要。然而，系统内部行为中离散、连续行为交织，极其复杂；而外界动态不确定环境更进一步加剧了相关系统行为复杂度，使得相关系统的可信构造与保障难以进行。针对此问题，我们提出了一种基于形式化建模与验证的可信构造与保障方法。首先我们提出了一种面向可重构系统的基于场景的层次化建模语言，来对系统动态行为进行快速建模。基于此建模语言，我们在运行时对系统短期内行为进行快速建模与验证，从而对潜在不安全行为进行发现与预警。在此基础上，我们进行运行时细粒度控制参数自动生成，在发现潜在危险时，接管系统控制，保障安全。部分成果已在列控、工控等领域进行应用验证，取得广泛关注。

简介：卜磊，教授，博士生导师，现任南京大学软件学院副院长，兼任 CCF 系统软件专委副主任（执行）；主要研究领域涉及可信软件、软件工程、形式化方法等方面，部分创新性工作发表在相关领域重要期刊与会议如《中国科学》、TCAD、TC、TOSEM、TDSC、CAV、RTSS、ICSE、DAC等上；入选高校计算机专业优秀教师奖励计划、CCF-IEEE CS青年科学家奖、中创软件人才奖、NASAC青年软件创新奖等奖项，主持基金委青A、重点、国际合作等项目多项。

4. 报告人：杨志斌 教授 

题目：大模型增强的安全关键软件模型驱动开发与验证方法

摘要：大模型技术为航空、航天、装备软件研发体系现代化转型提供了难得机遇。首先,简要介绍航空航天领域的安全关键软件开发与验证过程、标准及智能化发展趋势。其次，介绍我们近几年来将大模型融入航空航天关键软件模型驱动开发与验证过程的探索，涉及综合化航电系统需求分析与生成、AADL软件架构模型构建、模型驱动安全分析与评估、验证性质自动生成、SCADE模型验证与测试的智能化增强、C/Rust代码自动生成、Rust源代码漏洞分析等方面。最后，简要介绍安全关键智能软件建模与验证方面的一些初步研究。

简介：杨志斌，男，博士，南京航空航天大学计算机学院教授、博士生导师，入选江苏省高层次人才“333工程”第二层次，长期从事安全关键软件开发与验证方法研究。主持/参与国家自然科学面上基金、青年基金、国防基础科研大型工业软件重点项目、国防基础研究重点、装发重大、国防基础科研、江苏省自然科学青年基金、航空科学基金等近20项课题。发表论文80余篇，申请专利49项，其中授权29项。中国计算机学会形式化方法专委委员、中国计算机学会抗恶劣环境计算机专委委员、中国航空学会计算与仿真分会委员、航空电子3A基础架构标准委员会委员。获国防科技进步二等奖（第一完成人）、中国航空工业集团科技进步二等奖、江苏省教学成果二等奖、江苏省研究生教学成果二等奖等奖项。

5. 报告人：蔡少伟 研究员 

题目：基于形式化方法的 Agent 行为安全检测与优化

摘要：随着LLM Agent逐步具备感知、规划与工具调用能力，局部执行风险可能传播演变为系统级安全威胁，保障运行流程的安全性可控至关重要。本报告介绍一套基于形式化方法的Agent安全检测与优化框架：首先，将用户意图转换为适于形式化分析的中间表示，在关键环节嵌入安全断言，并借助约束求解器检查执行计划与行为是否满足安全约束；随后，结合反例分析CEGAR，对风险执行路径实施回滚与修正。同时，将同类任务的执行流程沉淀为可复用的工作流模板，通过形式化验证持续优化，并用于指导后续用户意图的形式化转换与执行规划，形成从意图转换、安全验证到执行纠偏与模板复用的闭环，为提升主流 Agent 工具的风险防护能力提供技术支撑。

简介：蔡少伟，中国科学院软件所/北京航空航天大学，研究员，研究约束求解和形式化方法，主持国家自然科学基金重点项目和青年基金B类项目，获得领域顶级会议CAV、CP和SAT的最佳论文奖/杰出论文奖，多次获得国际SAT比赛和SMT比赛冠军，混合整数规划比赛MIPcc亚军。研究成果被集成到英伟达、微软、英特尔、华为、华大九天等公司的软件中，应用于EDA、处理器验证、操作系统验证、以及密码分析。担任SAT 2027会议程序委员会主席，曾在FMCAD、CP和SOCS等国际会议做特邀报告。

6. 报告人：王东霞 研究员 

题目：Agents4PLC：多智能体驱动的工业控制软件可信开发与验证

摘要：工业控制软件是高端控制装备的核心工业软件，是智能制造的“神经中枢”，但其开发长期依赖专家经验，存在效率低、验证难等问题。在“人工智能+制造”、“人工智能+软件”等背景下，人工智能正从辅助工具加速成长为软件研发的核心生产力。本报告将介绍Agents4PLC 系列工作，探索以大模型智能体驱动工业控制软件开发的智能化升级。我们通过构建多智能体协同开发框架，融合工业领域知识和规范，实现低资源域下贯通需求、设计、代码生成、测试与验证全过程的工控软件高效可信开发新模式。报告最后将对未来工作和潜在挑战进行展望。

简介：王东霞，浙江大学控制科学与工程学院研究员，工业控制技术全国重点实验室工业安全研究所副所长。新加坡南洋理工大学博士，牛津大学博士后。主要研究方向为多智能体系统，人工智能和工业软件。主持国家自然科学基金面上/青年项目，国电南自、晶泰科技等企业课题多项；相关成果发表于人工智能及软件工程领域的国际顶级会议与期刊如NeurIPS，ICML，ICLR，AAMAS，TSE，ASE，ISSTA，TDSC，TIFS等三十余篇；并担任多个国际顶级会议的程序委员会委员及领域主席。

7. 报告人：鲁金直 副教授

题目：面向智能系统的系统工程语义设计方法

摘要：随着大模型深度应用，智能与敏捷设计成为智能系统研制过程中的工程热点。本报告聚焦原创性国标多架构建模语言KARMA (GB/T 45803-2025)，详解其如何针对典型智能系统构建定制化建模方法论与领域本体及元模型库。同时，核心展现KARMA如何利用其语义建模与知识推理能力，结合大模型技术，为各类体系框架提供通用智能创成式设计与运用能力。最后通过人机智融合系统案例验证该技术路线的可行性，并探索智能系统设计新范式。

简介：鲁金直，北京航空航天大学航空科学与工程学院副教授，国家级青年人才, 发表学术论文100余篇，包括IEEE Trans on SMC、CJA、AEI等顶级期刊30余篇，担任中国系统工程学会应用与咨询工作委员会副主任委员等职务，获得过集团科技进步三等奖、全国信标委标准化先进个人奖励。作为创始人提出了多架构建模语言KARMA，目前在欧盟H2020项目QU4LITY中被应用于空客某型飞机的装配方案设计。KARMA语言作为工信部高质量专项《XXX软件开发及应用》的核心技术，被应用于XX工程，打通任务、体系、系统的全流程架构设计，实现了全生命周期架构的统一架构建模。

五、论坛组织委员会简介

1. 论坛组委会：胡春明 教授 

简介：胡春明，北京航空航天大学教授，博导。现任复杂关键软件环境全国重点实验室副主任，软件学院院长。担任中国计算机学会（CCF）系统软件专委会副主任，标准工委技术委员会主任。主要研究方向为计算机软件与理论、安全攸关软件开发方法、分布式系统、数据中心资源管理与调度等。曾获国家科学技术发明二等奖1项、中国电子学会科学技术进步奖3项。

2. 论坛组委会：詹乃军 教授 

简介：詹乃军，北京大学计算机学院博雅特聘教授，国家杰出青年科学基金获得者。之前，为中科院软件所研究员，中科院特聘研究员，中国科学院大学岗位教授，计算机科学国家重点实验室执行主任。分别在南京大学数学系（1989-1993）和南京大学计算机系（1993-1996）获得学士和硕士学位，在中国科学院软件研究所获得博士学位（1997-2000）。研究方向包括：形式化方法，实时、嵌入式、混成系统，程序验证等。任《Journal of Automated Reasoning》、《Formal Aspects of Computing》、《J. of Logical and Algebraic Methods in Programming》、《Research Direction: Cyber-Physical Systems》、《软件学报》、《计算机研究与发展》《电子学报》、《前瞻科技》等期刊编委，国际会议MEMOCODE和SETTA的指导委员会委员，多个国际会议程序委员会共同主席（如形式化方法旗舰会议FM 2021 和验证领域顶级会议TACAS 2027）和著名国际会议程序委员会委员（如CAV、RTSS、HSCC、ICCPS、EMSOFT等）；在著名国际会议和杂志发表论文170多篇，出版专著2部，编著6部，国际国内著名杂志专刊9辑等；获得ESWEEK 2026 Test of Time Award。现任CCF形式化方法专委主任。

3. 论坛组委会：金芝 教授

简介：IEEE / CCF / CAAI会士，北京大学教授，武汉大学弘毅客座特聘教授，武汉大学特色化示范性软件学院院长，高可信软件技术教育部重点实验室常务副主任。研究方向为软件需求工程方法学、智能化软件工程和知识工程。曾获高等学校科学研究优秀成果奖（科学技术）科技进步奖一等奖，CCF科学技术奖技术发明一等奖，CCF夏培肃奖，中创软件人才奖等，多次获ACM SIGSOFT杰出论文奖。

4. 论坛组委会：葛宁 教授

简介：葛宁，北京航空航天大学软件学院教授、博导，先进工业软件研究所所长，CCF形式化方法专委会、软件工程专委会委员，商飞工业软件创新中心研究员、中航机载共性预研部副主任、复杂装备AI+工业软件北京市重点实验室副主任。研究方向为形式化方法、智能软件工程、智能安全，取得学术论文、专利软著等成果120余项，参编专著3部，参与多项安全关键软件标准建设。成果在航天、航空、核电、华为等单位应用，有效提升了关键软件的研制效率和质量，获华为技术落地奖和特色化示范性软件学院十大技术成果。入选2024年高校计算机专业优秀教师奖励计划，获2026年软件学院联盟优秀教师提名奖。