| 摘要: |
| 信息物理融合系统(cyber-physical system, CPS)在安全攸关领域具有广泛的应用, 保障其安全性至关重要. 形式化验证是证明系统安全性的有效手段, 但在现实世界中的复杂CPS系统上应用仍面临挑战. 因此, 反例生成的方法被提出, 旨在通过寻找系统中违背安全规约的反例行为来证明系统的不安全. 现有的基于路径的CPS系统反例生成方法采用分治策略, 针对系统模型中各条路径上的行为空间分别进行探索, 能够有效发现系统中的不安全行为. 然而, 在大规模系统中, 这类方法面临严重的路径爆炸问题, 路径数量随着离散状态数目指数级增长, 反例生成的效率和性能显著下降. 为缓解反例生成中的路径爆炸问题, 基于系统模型与规约提出路径过滤与动态选择两种技术. 首先, 设计面向规约的路径过滤方法, 通过分析系统规约的语法树和路径上的行为约束, 快速过滤不可能包含不安全行为的路径. 其次, 引入多臂老虎机算法来指导反例生成过程中路径的动态选择, 动态调整用于探索不同路径的计算资源以最大化反例生成的性能. 在一系列经典测试案例上的实验结果表明, 所提方法显著缓解了路径爆炸问题, 提高了CPS系统反例生成的效率和性能, 将发现不安全行为的成功率提升了两倍以上. |
| 关键词: 信息物理融合系统 混成自动机 反例生成 面向路径 |
| DOI：10.13328/j.cnki.jos.007352 |
| 分类号: |
| 基金项目:国家自然科学基金(62232008, 62172200); 江苏省前沿引领技术基础研究专项(BK20202001) |
|
| CPS Falsification Based on Hybrid Automata Path Filtering and Dynamic Selection |
|
WANG Jia-Wan1,2, LIU Xi-Tong2, BU Lei1,3, LI Xuan-Dong1,2
|
|
1.State Key Laboratory for Novel Software Technology (Nanjing University), Nanjing 210023, China;2.School of Computer Science and Technology, Nanjing University, Nanjing 210023, China;3.Software Institute, Nanjing University, Nanjing 210093, China
|
| Abstract: |
| Cyber-physical system (CPS) is widely employed in safety-critical domains, making its safety assurance a critical concern. Formal verification serves as an effective approach for proving system safety but encounters challenges when applied to complex real-world CPS. Falsification has been proposed as an alternative, aiming to demonstrate system unsafety by identifying counterexample behaviors that violate specified safety properties. Existing path-oriented falsification methods for CPS utilize divide-and-conquer strategies to explore system behaviors along individual paths, effectively uncovering unsafe behaviors. However, in large-scale CPS, these methods are hindered by the path explosion problem, where the number of paths grows exponentially with the system’s discrete system modes, leading to significant reductions in falsification efficiency and performance. To address the path explosion issue in path-oriented falsification, this study introduces two novel techniques based on system models and specifications: path filtering and dynamic path 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 |
