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.