Efficient Optimization-Based Falsification of Cyber-Physical Systems with Multiple Conjunctive Requirements
Efficient Optimization-Based Falsification of Cyber-Physical Systems with Multiple Conjunctive Requirements
复制标题
DOI：
10.1109/case49439.2021.9551474
复制
发表时间：
2021-08
期刊：
影响因子：
--
通讯作者：
L. Mathesen;Giulia Pedrielli;Georgios Fainekos
中科院分区：
文献类型：
--
作者：
L. Mathesen;Giulia Pedrielli;Georgios Fainekos
基于优化的伪造或基于搜索的测试是一种用于网络物理系统（CPS）安全评估的自动测试生成方法。CPS安全评估由信号时序逻辑（STL）表达的高级系统需求指导。使用满意度鲁棒性作为定量度量，根据STL需求评估执行CPS模拟的轨迹。特别是，鲁棒性是与特定输入相关联的模拟系统轨迹与已知不安全集（即违反要求的搜索空间区域）之间的距离度量。违规的识别可以表述为一个优化问题，其中的输入是最小化鲁棒性函数的兴趣。事实上，如果相关的健壮性为负，则输入会伪造需求。在这项工作中，我们特别考虑了多个需求决定不安全集的情况。由于执行CPS模拟的计算负担，从业者经常通过组合需求组件并获得所谓的“联合需求”来同时测试所有系统需求。由于鲁棒性函数可能“掩盖”单个连接需求组件的贡献，连接需求可以挑战基于优化的证伪方法。我们提出了一种新的算法，最小贝叶斯优化（minBO），它通过考虑连接需求的每个组成部分的贡献来处理这个问题。我们展示了minBO优化算法在应用于一般非线性非凸优化问题以及应用于现实证伪应用时的优势。
Optimization-based falsification, or search-based testing, is a method of automatic test generation for Cyber-Physical System (CPS) safety evaluation. CPS safety evaluation is guided by high level system requirements that are expressed in Signal Temporal Logic (STL). Trajectories from executed CPS simulations are evaluated against STL requirements using satisfaction robustness as a quantitative metric. In particular, robustness is the distance metric between the simulated system trajectory, associated to a specific input, and the known unsafe set, i.e., regions of the search space that violate the requirements. Identification of violations can be formulated as an optimization problem, where inputs that minimize the robustness function are of interest. In fact, an input falsifies a requirement if the associated robustness is negative. In this work, specifically, we consider the case where multiple requirements determine the unsafe set. Due to the computational burden of executing CPS simulations, practitioners often test all system requirements simultaneously by combining the requirement components and obtaining so-called “conjunctive requirements”. Conjunctive requirements can challenge optimization-based falsification approaches due to the fact that the robustness function may “mask” the contributions of individual conjunctive requirement components. We propose a new algorithm, minimum Bayesian optimization (minBO), that deals with this problem by considering the contributions of each component of the conjunctive requirement. We show the advantages of the minBO optimization algorithm when applied to general non-linear non-convex optimization problems as well as when applied to realistic falsification applications.