基于鲁棒性引导的黑盒检查的网络物理系统证伪
Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking
摘要：
对于详尽的形式化验证，工业规模的网络物理系统（CPS）通常太大和复杂，而轻量级的替代方案（例如，监测和测试）引起了工业从业人员和学术研究人员的关注。伪造是利用随机优化的CPS的一种流行测试方法。在最先进的证伪方法中，先前证伪试验的结果被丢弃，并且我们总是试图在没有任何先验知识的情况下证伪。为了简洁地记忆CPS模型的先验信息并加以利用，我们采用了黑盒检查（BBC），这是自动机学习和模型检验的结合。此外，我们加强了BBC使用STL公式，这是伪造的基本工具的强大语义。我们的实验结果表明，我们的鲁棒性指导的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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
