来源 :科大国创2023-12-04
随着国家、社会和人们日常生活对软件系统的依赖程度日益增长，软件成为信息化社会不可或缺的基础设施，复杂软件系统的正确性、安全性和可靠性日益凸显。安全攸关软件的高可信性质成了保障国家安全、保持经济可持续发展、维护社会稳定和保护人们生命财产安全与个人隐私等的关键。
12月1日至3日，中国软件领域规模最大、影响最广的学术会议——CCF中国软件大会(ChinaSoft 2023)在上海国际会议中心召开。2023年CCF中国软件大会（CCF ChinaSoft 2023）由CCF主办，科大国创参与支持。CCF理事长、大会执行委员会荣誉主席、中国科学院院士梅宏，上海市经济和信息化委员会主任张英，中国科学院院士、复旦大学校长金力致辞。何积丰、于全、徐宗本、柴洪峰、王义等5位国内外院士和业内专家蒋铭到会做特邀报告。院士林惠民、徐宗本、梅宏、吕建、柴洪峰、王怀民、张宏科出席大会相关论坛。
本届中国软件大会聚焦“智能化软件创新推动数字经济与社会发展”主题，汇聚学术界和产业界的专家学者交流学术、碰撞思想，以期超前谋划，踩准步点，推动我国软件技术与产业发展。
在形式化方法与应用论坛上，科大国创董事、中央研究院副院长纪金龙博士受邀进行主题报告，题目为“形式化方法在自动驾驶软件设计中的应用”。在自动驾驶软件中，自动紧急制动技术（AEB）能够有效预防车辆碰撞事故的发生，是当前汽车主动安全技术领域的研究热点之一。该报告重点概述了如何将形式化方法用于验证AEB算法的正确性，并分享了科大国创在形式化建模、算法验证、以及代码验证方面的一些尝试与应用成果。
当前，形式化方法已广泛应用于国防军工、航空航天等安全攸关领域。科大国创作为国内首批接触并从事形式化方法研究的团队之一，积极布局形式化技术落地。目前，科大国创已建立了高可信软件质量保障体系，全方位全流程给予代码稳定防护。此次大会，科大国创向与会嘉宾重点展示了两款形式化工具：科创瀚海静态分析工具和科创星云验证工具。
科大国创高可信软件质量保障体系全景图
科创瀚海静态分析工具
科创瀚海静态分析工具是一款采用符号执行与静态分析等相关技术通过对源代码静态扫描排查、挖掘、定位代码隐蔽缺陷，实现源代码全方面“体检”的分析工具。公司深耕静态分析领域多年，了解用户使用分析工具习惯，在开发了自动修复等创新性功能的同时，在安装至使用环节都注重提升用户基础使用体验。工具支持开发、测试等多场景应用，可提供以用户为中心的合规可视化报告，并支持定制拓展。
科创星云验证工具
科创星云验证工具作为一款能够使用数学证明的手段对计算机系统进行建模、规约、推理和验证，保证安全攸关系统的可靠性的形式化验证工具。平台采用了演绎推理的形式验证技术，可以根据验证者提供的有关程序需求功能的形式化描述（规约），基于霍尔逻辑（Hoare Logic）和形状图逻辑（Shape Graph Logic）对C程序进行演算，并使用自动定理证明技术来验证程序的行为与规约的一致性，使用户可以在软件开发的早期阶段就可以通过形式验证，提高软件系统的质量和可信度，以帮助用户开发出更加安全和可靠的高可信软件。
科大国创在高可信软件
领域沉淀研发二十年，致力于推动程序分析与验证理论进步，已经实现高可信软件技术的实用化，覆盖多个行业龙头客户和国家级项目。公司高可信分析工具集曾荣获CCF软件大会一等奖，是填补国内空白和解决“卡脖子”难题的关键技术，在国内国际处于领先地位，让中国人在关键软件领域有一席之地。高可信软件分析与验证技术可应用于航空航天、国防军工、轨道交通、智能汽车、金融、能源等安全攸关领域的高可信软件开发，在当今和未来的智能化时代，应用前景十分广阔。