高可信嵌入式软件工程技术论坛

---

嵌入式软件在航天、航空、轨交、汽车、核能等领域广泛应用，是重大装备关键功能的主要实现载体。随着“软件定义装备”特征的不断深化，国家重大工程对可信嵌入式软件的需求更加突出。同时，针对嵌入式软件的软件工程和形式化方法研究也一直都是学术界的重要关注点。

本论坛由航天502所高可信嵌入式软件工程专业实验室和北京轩宇信息技术有限公司发起，旨在加强工业需求和学术前沿融合，为工业界现实问题凝练和学术界成果更好服务国家重大需求架起桥梁。论坛已在ChinaSoft 2020举办一次，并将持续举办下去，打造学术界和工业界探讨可信嵌入式软件的交流平台。 本届论坛将邀请来自工业界和学术界的多位专家，一方面，分享当前国家重大工程中嵌入式软件的发展趋势、案例、科学问题和挑战，另一方面，分享国内学界在嵌入式软件分析、测试、验证以及智能软件工程方面的最新研究进展。

论坛主席和主持人：

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

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

论坛支持单位：

航天502所

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

日程安排：

时间：2021年12月24日（星期五），14:00~18:00

论坛议程：

论坛报告嘉宾简介：

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

摘要： 中断驱动型程序在航天器等安全关键领域广泛应用。由中断并发导致的缺陷长期以来都是工程中最难解决的可信问题之一，曾有多次航天器故障均由此类缺陷引发。虽然国内外开展了一些研究，但截止当前对这类缺陷的自动化检测仍难以满足实际需求。报告将分享502所研究团队近期围绕中断并发缺陷自动化检测所作的工作，首先介绍针对近10年真实中断并发缺陷所做的一项大规模缺陷特征实证研究，然后介绍单变量原子性违背模式检测的研究进展，最后对未来工作和挑战进行展望，希望与产研各界携手攻关解决。

简介： 陈睿，航天科技集团502所研究员，轩宇信息软件工具研发部部长，CCF形式化方法专业委员会委员。长期从事航天嵌入式软件可信保障技术的研究，以及相关工具软件的研制。先后主持和参与国家自然科学基金、国防科工局预研、863计划等项目10余项，发表论文20余篇，拥有软件测试领域的专利20余项。主持研制了覆盖嵌入式软件测试全过程的完整工具链产品，在我国载人飞船和空间站、嫦娥系列探测器、北斗导航卫星等绝大部分飞行软件的开发测试中广泛应用，并在国内率先通过国际功能安全认证，在军民各领域的50余家单位实现了对国外产品的替代。获北京市科技进步一等奖。

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

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

简介： 陈立前，国防科技大学计算机学院副教授。主要从事程序分析与验证、抽象解释相关研究。在ACM/IEEE Transactions、POPL、FSE等期刊会议上发表论文60余篇，曾获ACM SIGSOFT杰出论文奖，出版教材译著3部。研究成果获省部级科技进步一等奖1项、二等奖1项。部分成果已在航天、国防等领域重大工程中应用。

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

摘要： 随着安全领域软件要求的不断提高，对航空机载软件的测试覆盖率要求也逐步增加，从需求覆盖、语句覆盖，到判定覆盖，再到MC/DC覆盖。软件测试对不同软件结构的覆盖率越来越高，测试用例的选用越来越全面；但对于多模块或多单元的软件来说，不同单元之间的关系仍未得到全面测试。本报告以软件单元之间的不同关系入手，分析软件测试应关注或应覆盖的不同软件单元之间的数据关系和控制关系，同时对比国内外使用的不同耦合覆盖分析工具之间的优劣，以及是否采用工具执行覆盖率分析的优劣。最后报告对该方法在军民用飞机机载软件上不同的应用及裁剪要求进行说明和展望。

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

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

摘要： 随着互联网技术的快速发展，开源软件、开发者社区、软件问答平台等成为软件开发的新形态。它们在积累大量软件相关数据（包括源代码、注释和问答等）的同时，也蕴含了许多对软件开发和质量保障有用的知识。然而，不同于自然语言文本，源代码具有语法和深层语义依赖特征，如何利用好这些软件知识，并对软件的自动化开发和维护产生帮助面临着巨大的挑战。针对该挑战，通过有效捕捉源代码特有的语法语义等信息，我们研究了基于神经网络的源代码语义表征、源代码注释自动生成、代码推荐与生成、代码缺陷\漏洞自动检测等方法，研发了相应的智能辅助工具集，从而帮助开发者更高效的理解代码、编写代码和保障代码质量。

简介： 王旭，北京航空航天大学软件学院副教授、博导，CCF会员。主要研究方向为智能化软件工程。在ICSE、ASE、ASPLOS等国内外会议期刊上发表学术论文40篇，获国家发明专利授权13项、软件著作权11项，积极参与TSE、ASE、ICSME、中国科学等国内外会议期刊的组织和审稿工作。主持国家自然科学基金面上项目、青年项目、国家重点研发计划子课题等6项，作为核心骨干参与国家科技部和基金委重大项目7项，负责研发的智能化软件开发工具集及支撑环境、服务化软件开发与运行云平台等系统在航空航天、智慧城市等领域的软件开发中得到应用。

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

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

简介： 王璐，西安电子科技大学计算机科学与技术学院副教授。2018年12月于西安电子科技大学获软件工程专业首批博士学位（导师：李青山教授），2021年获陕西省优秀博士学位论文。目前任中国计算机学会软件工程专委会、系统软件专委会委员、首批CCF传播大使。主要研究方向为软件演化与自适应、微服务与智能化运维AIOps。相关研究成果在IEEE Transactions、ICSE、FSE等期刊会议上发表论文30余篇，并用于支持军事电子信息系统演化、航空航天软件运维治理、华为openEuler操作系统研发等国产自主可控软件的发展中。

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

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

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

7. 徐子川：针对航天软件的验证可靠性提升及加速方法

摘要： 如今航空航天的软件工程正处于飞速发展的阶段，航天软件的规模和复杂性急剧增加，其中如何提高验证的可靠性，避免已经发生的软件问题不再重犯以及如何尽可能的缩短软件仿真验证的时间成为了航天软件验证工程中两个亟待解决的挑战。本报告首先介绍了基于分布式FPGA的仿真验证加速方法，采用多FPGA组成分布式平台以硬件仿真的形式突破现有仿真加速技术速度和可扩展性方面的瓶颈，其次介绍了对如何使用AI方法解决软件缺陷检测结果的误报情况，对文本形式和多模态图形式的源代码进行处理，并利用一些深度方法达到精确检验，尽量减少误报的效果，最后报告分享了目前工作的进展。

简介： 徐子川，大连理工大学副教授、博士生导师。2008年和2011年从大连理工大学获得学士和工学硕士学位，2016年从澳大利亚国立大学获得博士学位，后于伦敦大学学院从事博士后。入选大连市海外高层次人才、青年科技之星、留创计划、大连理工大学星海优青。荣获2017年入选大连理工大学“星海骨干”计划、2019年入选大连理工大学“星海优青”计划。2020年入选大连市“本地全职高层次人才（青年才俊）”计划等称号。主持国际自然科学基金青年、面上项目，企业项目多项。研究方向边缘计算、大数据、网络虚拟化、无服务器计算等。在相关领域发表国际期刊会议论文100余篇，其中包括计算机学会推荐A、B类期刊会议50余篇。担任17家国际期刊审稿人，包括IEEE Trans.系列汇刊（TPDS、TMC、TC、TCOM、TII、TSC、TNSM）。担任ICSE 2019的Web Chair及多次国内外会议PC Member。担任2020年全国计算机体系结构学术年会分论坛主席。担任中国指挥与控制学会空中多智能体协同控制专业委员会委员。

论坛主席与主持人介绍：

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

简介： 研究员，航天科技集团五院502所计算机应用专业硕士毕业，现任航天科技集团五院502所空间飞行器软件检测站业务总监。长期从事航天嵌入式软件研发、测试以及测试工具研发工作。曾获国防科技进步奖二等奖、军队科技进步一等奖。近年来主要专注于嵌入式软件可信保证技术研究和工具研发，承担了国家自然基金、863、核高基等多项软件相关研究课题。

2. 论坛主席：陈睿

简介： 陈睿，航天科技集团502所研究员，轩宇信息软件工具研发部部长，CCF形式化方法专业委员会委员。长期从事航天嵌入式软件可信保障技术的研究，以及相关工具软件的研制。先后主持和参与国家自然科学基金、国防科工局预研、863计划等项目10余项，发表论文20余篇，拥有软件测试领域的专利20余项。主持研制了覆盖嵌入式软件测试全过程的完整工具链产品，在我国载人飞船和空间站、嫦娥系列探测器、北斗导航卫星等绝大部分飞行软件的开发测试中广泛应用，并在国内率先通过国际功能安全认证，在军民各领域的50余家单位实现了对国外产品的替代。获北京市科技进步一等奖。