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

Clc Number:

TP311

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    Cyber-Physical Systems (CPS) find extensive applications in safety-critical domains, making it crucial to ensure their safety. Formal verification is a powerful technique for proving system safety, but its application in complex, real-world CPS remains challenging. Falsification is therefore proposed, which aims to prove the unsafety of a system by identifying counterexample system behaviors that violate given safety properties. Existing path-oriented CPS falsification methods employ divide-and-conquer strategies, exploring system behavior along system paths, and can discover unsafe behaviors effectively. However, in large-scale CPSs, these methods face the serious challenge of path explosion. As the number of discrete system modes increases, the number of paths grows exponentially, leading to a notable decrease in falsification efficiency and performance. To mitigate the path explosion problem during path-oriented falsification, this paper proposes two techniques based on the system model and specification: path filtering and dynamic path selection. Firstly, we introduce a specification-driven path filtering technique that rapidly filters out paths unlikely to contain unsafe behaviors by analyzing the syntax tree of system specifications and the constraints on behaviors along each path. Secondly, we employ a multi-armed bandit algorithm to dynamically select paths to be falsified during the falsification process, adaptively adjusting computational resources allocated to explore different paths to maximize performance. Experimental results on a series of classical benchmarks show that our techniques significantly alleviate the path explosion issue and improve CPS falsification performance, leading to a twofold increase in the success rate of identifying unsafe system behaviors.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 26,2024
  • Revised:October 14,2024
  • Adopted:
  • Online: December 10,2024
  • Published:
You are the firstVisitors
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