软件学报

作者：杨紫萱，曾霞，任勐鑫，王建林，曾振柄，杨争峰

单位：杨紫萱，华东师范大学 软件工程学院, 上海 20006211,曾霞，西南大学 计算机与信息科学学院, 重庆 40071502,任勐鑫，河南大学 计算机与信息工程学院, 河南 开封 47500103,王建林，河南大学 计算机与信息工程学院, 河南 开封 47500104,曾振柄，上海大学 理学院, 上海 20044405,杨争峰，华东师范大学 软件工程学院, 上海 20006206

关键词：连续动力系统;障碍证书;PAC;区间线性化;混合整数规划

基金：国家重点研发计划(2022YFA1005101); 国家自然科学基金(12171159, 62272397); 上海市可信工业互联网软件协同创新中心; “数字丝绸之路”上海市可信智能软件国际联合实验室项目(22510750100)

连续动力系统安全验证是一个重要的研究问题, 多年来各类验证方法所能处理的问题规模非常受限. 对此, 对于给定的连续动力系统, 提出通过反例制导方法生成一组组合式概率近似正确(PAC)障碍证书的算法, 最终给出无限时间范畴安全验证问题在概率统计意义下的形式化描述. 通过建立和求解基于大M法的混合整数规划方法, 将障碍证书的求解转化为约束优化问题. 通过微分中值定理将非线性不等式进行区间线性化. 最后, 实现组合式PAC障碍证书生成工具CPBC, 并在11个基准系统上评估其性能. 实验结果表明, CPBC均能成功验证每个动力系统在指定不同的安全需求阈值下的安全性. 与现有方法相比, 所提方法可以更高效地为复杂系统或高维系统生成可靠的概率障碍证书, 验证的样例规模已高达百维.

来源：2025年第5期

《软件学报》期刊编辑部

查看软件学报杂志2025年第5期