2023年CCF中国软件大会（CCF ChinaSoft 2023）由CCF主办，CCF系统软件专委会、形式化方法专委会、软件工程专委会以及复旦大学联合承办，将于2023年12月1-3日在上海国际会议中心举行。
本次大会主题是“智能化软件创新推动数字经济与社会发展”，学术、工业、教育、竞赛等分论坛活动40余场，期待您的参与！
目前大会火热报名中！
CCF ChinaSoft 2023官方首页：
http://chinasoft.ccf.org.cn/
点击文末“阅读原文”或扫描下方二维码进入官方注册通道:
https://conf.ccf.org.cn/chinasoft2023
✦ +
+
论坛巡礼
论坛名称：高可信嵌入式软件智能化开发与测试论坛
时间: 2023年12月1日（星期五），14:00 – 18:00
地点: 上海国际会议中心，5F会议室
论坛简介：
嵌入式软件在航天、航空、轨交、汽车、核能等领域广泛应用，是重大装备关键功能的主要实现载体。随着人工智能技术的飞速发展，嵌入式软件开发测试方法正发生深刻的变革。一方面，嵌入式软件自身正在成为人工智能的实现载体，另一方面，智能化软件工程新方法也成为高可信、高效率研制嵌入式软件的重要支撑。
本论坛由航天502所高可信嵌入式软件工程专业实验室和北京轩宇信息技术有限公司发起，旨在加强工业需求和学术前沿融合，为工业界现实问题凝练和学术界成果更好服务国家重大需求架起桥梁，至今已在CCF ChinaSoft 举办3届，致力于成为学术界和工业界探讨可信嵌入式软件的交流平台。
本届论坛聚焦高可信嵌入式软件智能合成和分析测试方向，将邀请来自工业界和学术界的多位专家在相关方向共同探讨工业界挑战和学术研究前沿。
日程安排
Schedule
论坛主席
Forum Chairmen
顾斌
五〇二所
航天科技集团502所研究员，博士生导师。主要研究方向为航天器控制、可信软件、软件智能化开发和形式化方法等。
江云松
北京轩宇信息技术有限公司
航天科技集团502所研究员，轩宇信息总经理。长期从事航天嵌入式软件质量保证、软件测试等工作。带领团队建立了覆盖软件研制全生命周期的保障技术体系和工具类，在载人航天、深空探测、北斗导航等重要航天领域实现自主可控工具替代。主持并参与国防科工局某重点验证项目与研发项目，完成了智能软件测试、缺陷测试等多个装备发展部的课题。获中国专利奖、中国质量协会质量技术奖、航天贡献奖等。
陈睿
北京轩宇信息技术有限公司
博士，航天科技集团502所研究员，轩宇信息副总经理，CCF形式化方法专委会执行委员。长期从事嵌入式软件可信保障技术的研究，以及相关工具软件的研制。负责研制了覆盖嵌入式软件测试全过程的完整工具链，推动程序分析、符号执行、形式化验证等技术工具化并解决国家重大需求，在载人飞船和空间站、嫦娥系列探测器、北斗导航卫星等绝大部分飞行软件的开发测试中广泛应用，在军民200余家单位实现了对国外产品的替代。获北京市科技进步一等奖、航天贡献奖。
论坛嘉宾
Forum Guests
陈小红
华东师范大学
华东师范大学软件工程学院副教授，主要研究方向为基于环境建模的需求工程、需求形式化验证以及IoT最终用户编程。主持并参与了多项国家自然科学基金项目、重点研发、863、973项目以及省部级项目，主要工作包括基于环境建模的功能需求建模、需求形式化建模与验证、基于投影的需求分析、基于用户意图的IoT最终用户编程、IoT智能系统的需求确认等，在国内外知名期刊、会议发表论文50余篇。
报告题目：
基于软件IP的嵌入式软件需求描述语言
报告摘要：
本课题目的是在分析提炼嵌入式软件需求特征的基础上，并在本重大项目的“智能合成”目标以及“基于软件IP”的基本策略指导下，探索从嵌入式软件任务意图的自然语言描述到基于软件IP需求描述语言的（半）自动转换。主要工作包括从嵌入式软件任务意图等自然语言文档出发的，结合自然语言处理技术，研究嵌入式软件多维需求信息的自动提取方法，以及需求问题空间解耦和综合分析方法，定义基于软件IP的嵌 入式软件需求规约描述语言，探索从需求分析结果到基于软件IP需求描述语言的自动转换方法，并研制相应的支撑工具。
王淑灵
中科院软件所
中国科学院软件研究所副研究员，硕士生导师。2008年于北京大学数学科学学院获得博士学位，2008年至2012年分别于联合国大学国际软件技术研究所和中科院软件所从事博士后工作。研究方向为形式化方法、系统形式建模与验证、交互式定理证明等。在TOSEM、Computer Journal、CAV、FM、RTAS等发表论文30余篇。
报告题目：
面向嵌入式系统的软件IP知识建模与构造
报告摘要：
随着嵌入式系统实现的功能越来越多，软件规模变得越来越庞大和复杂，安全攸关领域对软件可靠性要求越来越高。针对如何高效开发可靠的嵌入式软件这一重大挑战，本报告将介绍基于软件IP的方法。软件IP（Intellectual Property）是具有知识产权的可复用的软件知识实体，是软件智能合成的基石。本报告将介绍面向嵌入式系统的软件IP通用模型：知识模型-形式模型-实现。这三层结构充分考虑了嵌入式系统的关键特性、系统对环境和平台的假设、软件中间知识的表示和使用、模型组装的正确性, 以及模型与实现之间的关系。此外，为了方便软件IP的使用，本报告从不同的使用目的（关注点）出发，介绍软件IP的各种视图。最后，本报告将展示软件IP工具以及知识库等相关工作。
董云卫
西北工业大学
博士，西北工业大学计算机学院教授、博士生导师，中国计算机学会杰出会员、中国计算机学会形式化方法专委会常委、陕西省计算机学会理事。主持国家自然基金重大项目课题“基于软件IP的软件智能合成及优化”等10余项科技项目。主要研究方向：软件智能合成控制软件理论与方法、智能软件测试、模型驱动开发方法和信息物理融合系统。获得陕西省首届杰出青年人才奖、中国软件杰出人才提名奖、陕西省科技进步等三等奖1项、国防科技成果三等奖2项奖和CCF科技成果二等奖1项。
报告题目：
面向控制软件合成的软件架构定义语言
报告摘要：
为了解决程序合成中的软件规模化合成等问题，我们提出了一种面向控制软件系统架构合成的架构定义语言，用来表达控制软件架构中的数据流、控制流及其时序依赖关系。控制架构作为软件开发意图理解到软件程序代码合成的过渡框架，把程序合成过程分成：需求—架构—程序框架—程序代码补全等四个阶段。报告结合航天器控制软件智能合成案例应用研究，介绍语言定义的软件模型类型、实现的语义以及模型组合与精化的模型语法范式。
马智
西安电子科技大学
西安电子科技大学准聘副教授，2022年于航天科技集团502所获得博士学位。主要研究领域为操作系统、嵌入式软件和形式化方法，长期致力于我国空间操作系统的设计和验证工作，参与多个国家重点、重大项目。
报告题目：
嵌入式软件合成过程及产品的质量保障
报告摘要：
嵌入式软件已经被广泛部署在各类航天器系统中，其存在的缺陷可能导致航天器的运行出现错误，嵌入式软件的可靠性和安全性是实现航天器系统“零缺陷”的前提。形式化方法是严格保证软件高度可靠和安全的有效手段，然而将其直接应用于实际工程项目仍面临巨大挑战，存在性质提取不充分、效率低和不准确的问题。为此，本报告主要介绍面向航天嵌入式软件的形式化性质挖掘技术。首先提出领域内规范化需求建模方法，引入知识图谱构建领域词库并制定结构化语义模板，在模型层面为性质的准确挖掘提供语义支撑；随后提出形式化性质自动挖掘框架，以需求模型为对象充分挖掘软件程序应具备的性质，同时结合自然语言处理和机器学习技术构建自动化过程，提升性质挖掘的效率；最后，进一步展望形式化方法在航天领域的应用前景。
李晓锋
北京控制工程研究所
研究员，北京控制工程研究所软件中心副主任，航天五院软件专家，CCF软件工程专委执行委员、嵌入式系统专委执行委员。主要研究领域：可信软件、软件自动化、自适应软件演化等。长期从事星载嵌入式软件开发和相关研究工作，作为项目负责人，完成了深空探测系列、星网星座等多项国家航天重大工程的软件研制，先后主持和参加了10余个预研项目，获军队科技进步奖多项、国际发明展金奖2项，发表论文40余篇，获得专利50余项。
报告题目：
嵌入式软件智能合成验证与示范应用
报告摘要：
软件智能合成是提升嵌入式软件开发效率和质量的有效途径，也是当前软件工程领域的研究热点。报告首先概述航天器嵌入式软件研制现状和存在的问题;在此基础上,提出了基于IP的嵌入式软件智能合成方法,并阐述基于软件IP的智能合成开发模式、软件智能合成开发平台构建、软件智能合成开发模式有效性评价以及典型领域示范应用四方面需要解决的关键技术;最后,对软件智能合成技术未来的发展方向进行展望。
孙猛
北京大学
北京大学数学科学学院信息与计算科学系教授，主要研究领域为程序理论、软件形式化方法、信息物理系统、深度学习。主持及作为主要成员参与国家自然科学基金、重点研发计划等国家及省部级项目十余项，在TSE、ESEC/FSE、ICSE、AAAI、FM等期刊及会议发表论文百余篇，获TASE2015、SBMF2017等多个国际会议最佳论文奖，任ICFEM2018、TASE2023等国际会议程序委员会主席，FM2019、TACAS2019等多个国际会议程序委员会委员。
报告题目：
深度神经网络的语义鲁棒性
报告摘要：
由对抗样本导致的深度神经网络局部鲁棒性问题已经受到广泛关注。而对于高斯噪声等语义扰动，神经网络同样具有很高的敏感性。由于语义扰动的多样性和复杂性，已有工作仅关注对旋转、亮度等特定语义扰动的局部鲁棒性问题。在这一工作中，我们给出了语义扰动和局部语义鲁棒性的形式化定义，这一定义可以涵盖当前人们关心的大部分语义扰动类型，在此基础上，我们给出了一种基于统计的方法，用于验证神经网络对于一般语义扰动的局部鲁棒性。在CIFAR-10和ImageNet上的实验表明，与当前最先进的统计认证算法相比，我们的方法仅使用3.32%-6.55%的运行时间即可提供与之相同的理论保证。
蔡彦
中国科学院软件研究所
中国科学院软件研究所（计算机国家重点实验室）研究员、博士生导师。2014年于香港城市大学获博士学位。研究方向包括软件安全、程序分析与测试、RISC-V软件、自动驾驶系统测试等。在软件工程领域ICSE、FSE、ISSTA、ASE、TSE等CCF A类国际会议和期刊发表论文30余篇。并先后担任多个学术职位（如ICSE 2022的AE共同主席、ICSE/FSE/ASE等PC 成员、期刊JSS的Associate Editor等）。
报告题目：
基于真实事故数据集的自动驾驶场景重建
报告摘要：
近年来，随着自动驾驶技术逐渐进入初期应用，在测试和实际使用过程中频繁发生的事故显示了该技术现阶段的不成熟，也给相关领域的测试人员带来了严峻的挑战。在初始模拟测试阶段，考虑到自动驾驶系统可能面临的未知场景，如何有效地构建具有挑战性的场景至关重要。我们提出了一种自动驾驶场景恢复及自动驾驶原型测试的方法和系统，基于取材自现实生活中的事故场景集，使用我们设计的M-CPS（Multi-channel Panoptic Segmentation, 多通道全景分割）全景分割模型，能够全面的、跨系统的、高可扩展性的完成场景恢复和自动驾驶原型的测试。我们基于主流的开源自动驾驶平台（例如Apollo/Carla）进行了测试，发现了多种可以导致自动驾驶原型发生事故的场景类型。相关论文发表于ISSTA 2023上。
陈睿
北京轩宇信息技术有限公司
航天科技集团502所研究员，轩宇信息副总经理，CCF形式化方法专委会执行委员。长期从事嵌入式软件可信保障技术的研究，以及相关工具软件的研制。负责研制了覆盖嵌入式软件测试全过程的完整工具链，推动程序分析、符号执行、形式化验证等技术工具化并解决国家重大需求，在载人飞船和空间站、嫦娥系列探测器、北斗导航卫星等绝大部分飞行软件的开发测试中广泛应用，在军民200余家单位实现了对国外产品的替代。获北京市科技进步一等奖、航天贡献奖。
报告题目：
安全攸关航天器智能软件的测试
报告摘要：
以深度学习为代表的人工智能技术在航天器等安全攸关CPS中已经得到应用。尽管人工智能技术为航天器的感知、控制和决策行为赋予智能，但人工智能与CPS都具有不确定的天然属性。对于安全攸关领域，如果这种不确定性没有得到恰当的处理，将会导致灾难性后果。对于承载航天器核心功能的智能软件，如何对其进行测试是航天器智能化时代面临的重要挑战之一。本报告以我国某探测器智能软件为背景，探讨我国航天器智能软件测试面临的需求和科学挑战，并对近期团队开展的研究和实践进展进行介绍。
冯劲草
上海工业控制安全创新科技有限公司
博士，上海控安可信软件创新研究院副院长，主要研究方向为形式化方法和需求工程。曾参与多项国家自然科学基金面上项目、联合基金项目，主要工作包括需求的形式化建模与分析，面向领域的形式化工程方法。与中国航发商发和卡斯柯信号有限公司等长期合作的工业界应用单位协同，对方法和工具在真实工业环境下进行应用验证。近些年在国内外知名期刊会议上发表了6篇文章。
报告题目：
基于嵌入式系统模型一致性分析与验证
报告摘要：
在安全攸关领域的嵌入式软件发过程中，不同阶段模型之间的不一致往往会导致严重的后果。航空领域中的DO-333标准明确要求低层需求模型（详细需求）应与设计（架构）模型一致。针对嵌入式控制系统软件研制过程中的需求模型与设计模型，探索一种保障需求模型和设计模型本身的正确性与验证模型之间的一致性方法。主要工作包括基于领域特征，研究需求建模语言和相应的系统性建模方法，进行需求形式化建模，结合设计阶段常用的模型语言lustre-v6，研究不同刻面的需求模型与设计模型的一致性分析技术，并开发相应的软件支撑工具，解决分析过程自动化和适应真实工业项目的问题。
