Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness
Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness
复制标题
DOI：
10.1007/978-3-030-81685-8_29
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Zhenya Zhang;Deyun Lyu;Paolo Arcaini;L. Ma;I. Hasuo;Jianjun Zhao
中科院分区：
文献类型：
--
作者：
Zhenya Zhang;Deyun Lyu;Paolo Arcaini;L. Ma;I. Hasuo;Jianjun Zhao
混合系统证伪是一种重要的网络物理系统质量保证方法，具有比穷举验证更具可扩展性和可行性的优点。在给定期望的时间规范的情况下，证伪试图找到违规的输入而不是证据保证。最先进的证伪方法通常使用随机爬山优化，该优化最小化了由其定量语义给出的时间规范的满足度。然而，已有研究表明，与规范中使用的信号的不同尺度(例如，转速和速度)有关的所谓尺度问题可能严重影响篡改的性能：在健壮性计算中，一个信号的贡献可能被另一个信号的贡献所掩盖。在本文中，我们提出了一种新的方法来解决这个问题。我们首先引入了一种新的稳健性定义，称为QB-稳健性，它结合了经典布尔满意度和定量稳健性。证明了QB-稳健性可以用来判断规范的满足程度，避免了其计算中的尺度问题。通过一种基于蒙特卡罗树搜索的形式规范结构上的证伪方法来利用QB稳健性。首先，树遍历法确定需要用来计算量化稳健性的子公式。然后，在树叶上进行数值爬山优化，旨在证伪这些子公式。我们在多个基准上的深入评估表明，我们的方法比经典的量化稳健性指导下的最新的证伪方法获得了更好的证伪结果，并且基本上不受规模问题的影响。
Hybrid system falsification is an important quality assurance method for cyber-physical systems with the advantage of scalability and feasibility in practice than exhaustive verification. Falsification, given a desired temporal specification, tries to find an input of violation instead of a proof guarantee. The state-of-the-art falsification approaches often employ stochastic hill-climbing optimization that minimizes the degree of satisfaction of the temporal specification, given by its quantitativerobust semantics. However, it has been shown that the performance of falsification could be severely affected by the so-calledscale problem, related to the different scales of the signals used in the specification (e.g., rpm and speed): in the robustness computation, the contribution of a signal could bemaskedby another one. In this paper, we propose a novel approach to tackle this problem. We first introduce a new robustness definition, calledQB-Robustness, which combines classical Boolean satisfaction and quantitative robustness. We prove that QB-Robustness can be used to judge the satisfaction of the specification and avoid the scale problem in its computation. QB-Robustness is exploited by a falsification approach based on Monte Carlo Tree Search over the structure of the formal specification. First, tree traversal identifies the sub-formulas for which it is needed to compute the quantitative robustness. Then, on the leaves, numerical hill-climbing optimization is performed, aiming to falsify such sub-formulas. Our in-depth evaluation on multiple benchmarks demonstrates that our approach achieves better falsification results than the state-of-the-art falsification approaches guided by the classical quantitative robustness, and it is largely not affected by the scale problem.