会议日程

郭向英（航天502所，北京轩宇信息技术有限公司）

陈睿（航天502所，北京轩宇信息技术有限公司）

论坛支持单位：

航天502所

北京轩宇信息技术有限公司

日程安排：

论坛议程：

1．陈睿：中断驱动型程序并发缺陷检测

2.陈立前：航天嵌入式软件静态分析

摘要：软件故障已成为航天系统失败的重要因素。源代码级程序错误仍是航天嵌入式软件中最突出的问题之一，数组越界、算术溢出、除以零、指针错误、数据竞争等问题仍经常发生。静态分析能够在编译时通过分析源代码来推断程序运行时性质，是提高航天嵌入式软件安全性与可靠性的一种重要技术。报告将从静态分析视角，分析航天嵌入式软件的代码特征及常见错误。在此基础上，介绍适合于航天嵌入式软件错误检测需求的静态分析技术。

3.陈刚：面向军民机的耦合覆盖分析方法研究及应用

简介：陈刚，航空工业第一飞机设计研究院（简称：一飞院)研究员，中国民航局机械系统专业适航委任代表，国际系统工程委员会成员。2005年和2008年从西安电子科技大学获得计算机科学学士和硕士学位，2016年从法国国立航空航天大学获得系统工程学硕士学位。法国在读期间曾参与法国民航总局NECTAR（新一代航空系统构型和架构）预研项目；在一飞院参与民用运输机MA700项目及多个军机型号项目的研制和机载软件管理，担任多个型号主任设计师，主要研究方向为机载软件适航符合性技术、系统工程等。

4.王旭：源代码智能开发及质量保障

5.王璐：航天软件的动态演化及可信保障研究

摘要：航天软件在投入运行后，极易受到不确定环境、非预期任务、或未知故障的影响，极易导致软件产生的重大错误。现有通过地面人工分析决策的方式不仅难以预先考虑到所有工况，也同时了耗费庞大的人力物力。因此，如何建立不确定环境下航天软件的动态演化能力，使其能不断调整自身以适应复杂多变的运行环境与任务需求，已成为确保航天软件稳定运行的关键问题。并且，如何确保该演化过程的可靠性，保证该过程对软件的调整正确合理，也是提升航天软件自身可信性的关键环节。因此，本次报告致力于探讨如何借助自主计算、智能化运维的思想，针对不确定环境的特征建立航天软件动态演化过程，并讨论如何为航天软件的演化过程提供可靠性保障。

6.蒋维：基于形式化技术的核电安全级DCS代码生成器

摘要：安全级DCS被称为核电站的“神经中枢”，是核电站重大关键性成套设备之一。由DCS搭建反应堆保护系统和安全专设系统以实现核电机组安全、平稳、高效运行。在DCS设备控制策略中，从控制逻辑图转换成控制代码，是确保安全的关键步骤。为了提高安全可靠性，“龙鳞”安全级DCS系统在研制过程中引入形式化方法，解决编译器“误编译”问题。同时保持了图形逻辑控制语义与控制器C语言语义的一致性，使得生成的代码免去重复测试与验证的工作，提高了固有安全性，降低了后端工作量。同时也面临兼容性、效率性和通用性等一系列新的问题亟待解决。

简介：蒋维，中国核动力研究设计院仪控工程中心研发副部长，CCF高级会员。主要研究方向嵌入式软件架构设计、微内核操作系统、形式化技术、可信编译器、研发体系建设。带领团队研发了我国首套军民融合安全级DCS平台，三代核电首套国产化堆芯测量系统中堆芯冷却检测系统（CCMS）和堆芯中子通量检测系统（CNFM）。获得全国技术质量一等奖，中核集团科技进步二等奖，参编标准2项，发表论文12篇，申请专利19项，软件著作权23项。