HyperPart-X: Probabilistic Guarantees for Parameter Mining of Signal Temporal Logic Formulas in Cyber-Physical Systems
摘要
Optimization-based falsification is an automatic test generation method for evaluating the safety of Cyber-Physical Systems (CPS) against formal requirements. In this work, we focus on temporal logic requirements and, more specifically on Parametric Signal Temporal Logic (pSTL). pSTL generalizes STL allowing to express the quantifiers of the logical operators as variables. This extends the falsification from searching for the inputs that violate the requirement to the inputs and the formula parametrizations that result into unsafe behaviors. The state-of-the-art Part-X, a recent algorithm for falsification, offers probabilistic falsification level sets and confidence-bounded results on inputs but is not tailored for pSTL. Our approach, HyperPart-X, builds on Part-X and solves the problem while also providing probabilistic guarantees on the estimated level set by adaptively branching the parameter space and intelligently sampling from both the parameter and input spaces in a coordinated and hierarchical approach. HyperPart-X is compared on synthetic functions and CPS benchmarks against uniform random and Part-X . Empirical results demonstrate that HyperPart-X returns level set estimates and guarantees, where Part-X fails to find a solution. Results also show that it can achieve the level set with the same associated confidence level as uniform random sampling using orders of magnitude less samples.