主题：基于路径空间遍历的有界验证途径及其应用

主讲人：卜磊

主持人：施智平

时间：2023年6月20日（周二）15:00

地 点：yl9193永利二层大会议室

主办单位：yl9193永利

主讲人简介：

卜磊，教授，博士生导师，现任南京大学软件学院副经理，兼任 CCF 系统软件专委秘书长；2010年在南京大学计算机与科学技术系获取博士学位；曾在CMU、MSRA等科研机构进行访学与合作研究；主要研究领域涉及软件工程、可信软件、形式化方法，研究工作集中在模型检验技术、实时混成系统、信息物理融合系统等方面，部分创新性工作发表在相关领域重要期刊与会议如《中国科学》、TCAD、TC、TDSC、TCPS、TPDS、RTSS、ICSE、ISSTA、ASE等上；入选国家级青年人才计划、高校计算机专业优秀教师奖励计划、CCF-IEEE CS青年科学家奖、NASAC青年软件创新奖、CCF青年人才发展计划、MSRA铸星计划等。

主讲内容简介：

人类社会正在进入软件定义一切的时代，软件系统的规模和复杂性增长进一步加剧，软件可信保障面临更加严峻的挑战。复杂软件系统中连续与离散行为交织、状态空间爆炸、非线性行为难以建模等障碍使得系统验证过程中的复杂性难以控制，现有方法与技术离处理实际问题需要存在较大差距。本报告系统地阐述我们为有效解决复杂系统验证过程中的复杂性控制问题所提出的基于路径空间遍历的有界验证途径。我们从单条路径状态空间验证出发控制整体验证的复杂性；通过路径中不可行片段的抽取进行路径空间缩减；设计新型浅同步语义规避组合状态空间爆炸；引入智能化动态迭代求解技术处理非线性约束难解问题；在此基础上，我们进一步将相关技术拓展至面向场景的复杂软件系统在线验证与控制生成，对软件系统行为可靠性进行系统性保障。基于上述工作，我们开发了复杂软件系统模型检验工具集BACH。与国际上同类相关工具相比，BACH在基准案例集上的性能明显超出，获得广泛关注与影响，并在列控、航天、物联网等领域得到实际应用验证。