软件所提出随机系统容忍障碍函数方法
近日，中国科学院软件研究所天基综合信息系统全国重点实验室针对传统随机系统安全规约难以容纳短暂、可恢复的非安全访问问题，提出容忍安全与容忍到达-规避性质及相应的容忍障碍函数方法，为随机系统的定量安全验证提供了新的理论工具和算法支撑。相关成果论文Tolerant Barrier Certificates for Stochastic Systems被第26届嵌入式软件国际会议EMSOFT 2026录用，并将发表于IEEE TCAD期刊，第一作者冯胜华副研究员。
随机动态系统广泛应用于机器人、嵌入式系统和信息物理系统等领域，用于描述受噪声、误差等随机因素影响的物理和计算过程。传统安全规约通常要求系统始终避开非安全区域，任何一次越界都会被判定为失败。然而在实际运行中，传感噪声、执行误差或环境扰动可能引起短暂的非安全偏离，但并不一定表示任务失败。由此，研究团队认为相比“是否曾经越界”，更有意义的指标是“累计越界次数”或“停留时间”是否控制在给定阈值内。
现有随机障碍函数主要用于判断系统是否进入非安全区域，难以直接给出累计非安全访问超过指定阈值的概率上界；动态规划和概率模型检测等方法通常依赖有限状态表示，也难以扩展到非线性、连续状态随机系统。
因此，研究团队提出了面向随机系统的容忍安全验证框架，用累计非安全访问刻画系统的安全风险：离散系统采用访问非安全集合的累计次数，连续系统采用在非安全集合中的累计占用时间，并据此定义容忍安全和容忍到达-规避性质，将安全规约由“零违规”拓展为“累计非安全访问不超过给定阈值”的概率性判断。进一步，研究团队构建了容忍障碍函数方法，根据系统所处区域设置不同的下降条件，并将障碍函数与累计访问次数或占用时间结合构造超鞅，推导非安全访问超过给定阈值的概率上界。针对具有多项式动力学和半代数状态集合的随机系统，研究团队将容忍障碍函数的合成转化为平方和规划问题，并基于Julia和MOSEK实现了原型工具。
容忍安全与容忍到达-规避性质
在离散与连续时间的容忍安全和容忍到达-规避四类任务上，容忍障碍函数方法在各基准中均成功合成障碍函数，并获得容忍安全性质的概率估计。蒙特卡洛实验表明，代表性案例计算得到的概率界与经验分布处于相近量级。可扩展性实验进一步验证了6至16维耦合随机系统，在16维情形下四类任务的求解时间均不超过约137秒。与计数器增广方法相比，容忍障碍函数方法直接在原状态空间中合成单个障碍函数，并可复用于不同非安全访问阈值，为含噪声嵌入式系统和信息物理系统的可靠性分析提供了新的形式化验证手段。
