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