Hybrid System Falsification Under (In)equality Constraints via Search Space Transformation
Hybrid System Falsification Under (In)equality Constraints via Search Space Transformation
复制标题
通过搜索空间变换在（不）等式约束下进行混合系统证伪
DOI：
10.1109/tcad.2020.3013073
复制
发表时间：
2020
影响因子：
2.9
通讯作者：
Hasuo Ichiro
中科院分区：
文献类型：
--
作者：
Zhang Zhenya;Arcaini Paolo;Hasuo Ichiro
由于连续动态导致无限的搜索空间，混合系统的验证本质上是困难的。因此，研究尝试集中在黑盒模型的混合系统伪造上，该技术旨在找到违反所需时间规范的输入信号。主要的伪造方法基于随机爬山优化，试图最小化由其鲁棒语义给出的时间规范的满意度。然而，在输入之间存在约束的情况下，这些方法变得不太有效。在本文中，我们使用搜索空间变换来解决这个问题，该变换首先将无约束搜索空间的点映射到受约束搜索空间的点，然后根据后一个搜索空间的鲁棒性值定义前一个搜索空间的适应度。基于这种搜索空间变换，我们提出了一种伪造方法，该方法在受约束空间中映射点的鲁棒性的指导下，在无约束空间上执行搜索。我们介绍了所提出方法的三个版本，它们在选择映射点的方式上有所不同。实验表明，所提出的方法优于最先进的约束伪造方法。
The verification of hybrid systems is intrinsically hard, due to the continuous dynamics that leads to infinite search spaces. Therefore, research attempts focused on hybrid system falsification of a black-box model, a technique that aims at finding an input signal violating the desired temporal specification. Main falsification approaches are based on stochastic hill-climbing optimization, that tries to minimize the degree of satisfaction of the temporal specification, given by its robust semantics. However, in the presence of constraints between the inputs, these methods become less effective. In this article, we solve this problem using a search space transformation that first maps points of the unconstrained search space to points of the constrained one, and then defines the fitness of the former ones based on the robustness values of the latter ones. Based on this search space transformation, we propose a falsification approach that performs the search over the unconstrained space, guided by the robustness of the mapped points in the constrained space. We introduce three versions of the proposed approach that differ in the way of selecting the mapped points. Experiments show that the proposed approach outperforms state-of-the-art constrained falsification approaches.