软件学报

作者：王佳宛，刘熹橦，卜磊，李宣东

单位：王佳宛，计算机软件新技术全国重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机学院, 江苏 南京 21002311,刘熹橦，南京大学 计算机学院, 江苏 南京 21002302,卜磊，计算机软件新技术全国重点实验室(南京大学), 江苏 南京 210023;南京大学 软件学院, 江苏 南京 21009303,李宣东，计算机软件新技术全国重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机学院, 江苏 南京 21002304

关键词：信息物理融合系统;混成自动机;反例生成;面向路径

基金：国家自然科学基金(62232008, 62172200); 江苏省前沿引领技术基础研究专项(BK20202001)

信息物理融合系统(cyber-physical system, CPS)在安全攸关领域具有广泛的应用, 保障其安全性至关重要. 形式化验证是证明系统安全性的有效手段, 但在现实世界中的复杂CPS系统上应用仍面临挑战. 因此, 反例生成的方法被提出, 旨在通过寻找系统中违背安全规约的反例行为来证明系统的不安全. 现有的基于路径的CPS系统反例生成方法采用分治策略, 针对系统模型中各条路径上的行为空间分别进行探索, 能够有效发现系统中的不安全行为. 然而, 在大规模系统中, 这类方法面临严重的路径爆炸问题, 路径数量随着离散状态数目指数级增长, 反例生成的效率和性能显著下降. 为缓解反例生成中的路径爆炸问题, 基于系统模型与规约提出路径过滤与动态选择两种技术. 首先, 设计面向规约的路径过滤方法, 通过分析系统规约的语法树和路径上的行为约束, 快速过滤不可能包含不安全行为的路径. 其次, 引入多臂老虎机算法来指导反例生成过程中路径的动态选择, 动态调整用于探索不同路径的计算资源以最大化反例生成的性能. 在一系列经典测试案例上的实验结果表明, 所提方法显著缓解了路径爆炸问题, 提高了CPS系统反例生成的效率和性能, 将发现不安全行为的成功率提升了两倍以上.

来源：2025年第8期

《软件学报》期刊编辑部

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