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.
翻译:为了进行彻底的正式核查,工业规模的网络物理系统(CPS)往往过于庞大和复杂,轻量级替代品(例如监测和测试)已经引起工业从业人员和学术研究人员的注意。 Falci化是CPS使用随机优化的一种流行测试方法。在最先进的伪造方法中,以往的伪造试验的结果被抛弃,我们总是试图在没有任何事先知识的情况下伪造。为了简明地记住以前关于CPS模型的信息并加以利用,我们采用了黑盒检查(BBC),这是自动化数据学习和模型检查的结合。此外,我们用STL公式的坚固的语义来增强BBC,这是伪造中必不可少的工具。我们的实验结果表明,我们以坚固性引导英国广播公司的模型超越了最先进的伪造工具。