CPS Falsification Based on Hybrid Automata Path Filtering and Dynamic Selection
Author:
Affiliation:

Clc Number:

TP311

  • Article
  • | |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • | |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

王佳宛,刘熹橦,卜磊,李宣东.基于混成自动机路径过滤与动态选择的CPS系统反例生成.软件学报,2025,36(8):3587-3603

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 26,2024
  • Revised:October 14,2024
  • Online: December 10,2024
You are the first2049861Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063