论文标题
具有鲁棒性引导的黑盒检查的网络物理系统的伪造
Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking
论文作者
论文摘要
为了进行详尽的正式验证，工业规模的网络物理系统（CPSS）通常太大且复杂，轻巧的替代方案（例如，监测和测试）吸引了工业从业者和学术研究人员的注意。伪造是使用随机优化的一种流行的CPS测试方法。在最先进的伪造方法中，先前的伪造试验的结果被丢弃，我们始终在没有任何先验知识的情况下试图伪造。为了简单地记住有关CPS模型的此类事先信息并利用它，我们采用了Black-Box检查（BBC），这是自动机学习和模型检查的组合。此外，我们使用STL公式的稳健语义增强了BBC，这是伪造的必不可少的小工具。我们的实验结果表明，我们的鲁棒性指导的BBC优于最先进的伪造工具。
For exhaustive formal verification, industrial-scale cyber-physical systems (CPSs) are often too large and complex, and lightweight alternatives (e.g., monitoring and testing) have attracted the attention of both industrial practitioners and academic researchers. Falsification is one popular testing method of CPSs utilizing stochastic optimization. In state-of-the-art falsification methods, the result of the previous falsification trials is discarded, and we always try to falsify without any prior knowledge. To concisely memorize such prior information on the CPS model and exploit it, we employ Black-box checking (BBC), which is a combination of automata learning and model checking. Moreover, we enhance BBC using the robust semantics of STL formulas, which is the essential gadget in falsification. Our experiment results suggest that our robustness-guided BBC outperforms a state-of-the-art falsification tool.
