Page 165 - 《软件学报》2025年第8期

3588 软件学报 2025 年第 36 卷第 8 期

selection. First, a specification-driven path filtering method is proposed to rapidly eliminate paths unlikely to contain unsafe behaviors by
analyzing the syntax tree of system specifications and the behavioral constraints of each path. Second, a multi-armed bandit algorithm is
adopted to guide the dynamic selection of paths during the falsification process, adaptively reallocating computational resources to optimize
performance. Experimental evaluations on several classical benchmark cases demonstrate that the proposed techniques effectively mitigate
the path explosion problem, significantly enhancing the efficiency and performance of CPS falsification. The success rate of identifying
unsafe system behaviors improves by more than twofold.
Key words: cyber-physical system (CPS); hybrid automata; falsification; path-oriented

信息物理融合系统 (cyber-physical system, CPS) 集成了计算、通信和控制这 3 大技术, 紧密融合计算过程与
物理过程, 是一类复杂的系统 [1,2] . 这些系统被广泛应用于国防军工、航空航天、智能交通、医疗救助等诸多安全
攸关领域. 其行为的复杂性以及应用场景的广泛与重要性, 使得确保这类系统能够安全可靠运行至关重要.
[3]
混成自动机 (hybrid automata) 作为一种强大的数学建模工具, 能够形式化地描述 CPS 系统中离散计算和连
续物理过程紧密交织的混合动态行为. 然而, 现有的混成自动机的形式化验证技术 [4] 大多局限于低维度, 线性或特
定动态行为特性的混成自动机模型 [5] , 难以应用于现实世界中日益复杂的大规模 CPS 系统. 因此, 近年来, 对 CPS
系统可靠性进行反例生成 (falsification) 被大量研究并在工业界应用.
CPS 系统反例生成方法旨在从系统模型中寻找违反系统规约的不安全行为, 从而证明系统不安全. 当前, 主流
的反例生成技术大多采用基于优化的方法, 在系统行为空间中寻找能够最小化系统规约鲁棒的行为 [6–12] . 在此基
础上, 基于路径的策略被应用于反例生成: 通过对系统的混成自动机模型进行遍历来生成路径, 再针对每条路径进
行基于优化的反例生成来寻找路径上的不安全的行为 [13,14] . 面向路径的反例生成方法尤其适用于内部具有不确定
性的 CPS 系统. 由于系统在不同路径选择下行为差异显著, 路径有助于更精确地控制不确定性系统的行为, 进而
更全面地探索覆盖其行为空间. 此外, 面向路径的方法通过分治策略层次化地求解问题, 将系统的复杂行为空间基
于离散路径分解为多个较小子空间并独立求解, 降低了优化问题的维度和复杂性, 进而提高了反例生成的性能. 目前,
[10]
较为成熟的 CPS 反例生成工具包括基于优化的工具 S-TaLiRo 、Breach 以及面向路径和优化的工具 SNIFF 等.
[14]
[11]
然而, 对于现实世界中的大规模 CPS 系统, 基于路径的反例生成方法容易面临严重的路径爆炸问题. 当系统
模型中存在大量离散状态时, 系统路径数量往往会呈指数级增长. 由于对每条路径进行基于优化的反例生成较为
耗时, 每次优化迭代都需要对系统的行为轨迹进行模拟计算, 因此, 当系统路径数量较大时, 系统整体反例生成的
耗时无疑会大幅增加. 而实际应用中, 对系统的可靠性进行反例生成分析往往会有时间或系统行为模拟次数的限
制. 当系统路径爆炸时, 每条路径被分配到的时间和计算资源都会非常有限, 导致路径上的系统行为空间难以被充
分探索, 系统整体的反例生成成功率也会相应降低.
在此背景下, 本文尝试从减少路径数目以及为路径合理分配计算资源这两个角度出发, 缓解 CPS 反例生成中
的路径爆炸问题, 提高反例生成性能. 首先, 传统的基于路径的反例生成方法通常仅依赖自动机的离散图结构来生
成路径, 然后对每条路径上的行为都进行探索检查. 但实际上, 系统在某些路径上的行为可能由于受路径上的约束
的限制, 一定不会违背规约. 因此, 本文提出了一种面向规约的路径快速探索与过滤方法, 根据系统规约的语法树
和路径上的约束, 基于约束求解器快速过滤掉一定不包含不安全行为的路径, 从而缓解路径爆炸. 其次, 传统方法
中通常会使所有路径平分计算资源, 逐条路径依次探索, 即每条路径进行反例生成时优化算法的迭代次数 (系统行
为的模拟次数) 相同. 因此, 本文进一步提出了基于多臂老虎机算法指导的路径动态选择的反例生成方法. 该方法
首先对各条路径都进行初步探索, 然后利用已探索的信息不断地动态选择更具有潜力的路径执行基于优化的反例
生成, 自适应地调整不同路径的计算资源分配, 从而最大化反例生成性能.
总之, 本文为提高 CPS 系统的安全性和可靠性, 提出了基于混成自动机路径过滤与动态选择的反例生成方法.
本文的主要贡献可以总结为以下几点.
• 针对基于路径的 CPS 系统反例生成方法, 提出了面向系统时序规约的路径过滤技术, 减少冗余路径, 缓解路
径爆炸问题;
• 针对需要反例生成的多条路径, 提出了基于多臂老虎机的路径动态选择策略, 充分利用系统路径的探索信
息, 智能化地为路径动态分配反例生成的计算资源, 提升系统反例生成的性能;