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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

HyperPart-X: Probabilistic Guarantees for Parameter Mining of Signal Temporal Logic Formulas in Cyber-Physical Systems

  • Tanmay Khandait,
  • Giulia Pedrielli

摘要

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.