Black-box runtime verification methods for cyber-physical systems can be used to discover errors in systems whose inputs and outputs are expressed as signals over time and their correctness requirements are specified in a temporal logic. Existing methods, such as requirement falsification, often focus on finding a single input that is a counterexample to system correctness. In this paper, we study how to create test generators that can produce multiple and diverse counterexamples for a single requirement. Several counterexamples expose system failures in varying input conditions and support the root cause analysis of the faults. We present the WOGAN algorithm to create such test generators automatically. The algorithm works by training iteratively a Wasserstein generative adversarial network that models the target distribution of the uniform distribution on the set of counterexamples. WOGAN is an algorithm that trains generative models that act as test generators for runtime verification. The training is performed online without the need for a previous model or dataset. We also propose criteria to evaluate such test generators. We evaluate the trained generators on several well-known problems including the ARCH-COMP falsification benchmarks. Our experimental results indicate that generators trained by the WOGAN algorithm are as effective as state-of-the-art requirement falsification algorithms while producing tests that are as diverse as a sample from uniform random sampling. We conclude that WOGAN is a viable method to produce test generators automatically and that these test generators can generate multiple and diverse counterexamples for the runtime verification of cyber-physical systems.

翻译：针对信息物理系统的黑盒运行时验证方法可用于发现系统错误，这些系统的输入和输出表示为随时间变化的信号，其正确性需求用时序逻辑进行规约。现有方法（如需求证伪）通常侧重于寻找单个违反系统正确性的反例输入。本文研究如何创建能够为单一需求生成多个多样化反例的测试生成器。多个反例可在不同输入条件下揭示系统故障，并支持缺陷的根源分析。我们提出WOGAN算法来自动创建此类测试生成器。该算法通过迭代训练一个Wasserstein生成对抗网络来实现，该网络对反例集合上均匀分布的目标分布进行建模。WOGAN是一种训练生成模型的算法，这些模型可作为运行时验证的测试生成器。训练过程在线执行，无需预先存在的模型或数据集。我们还提出了评估此类测试生成器的标准。我们在多个经典问题上评估训练后的生成器，包括ARCH-COMP证伪基准测试。实验结果表明，通过WOGAN算法训练的生成器与最先进的需求证伪算法同样有效，同时生成的测试案例具有与均匀随机采样相当的多样性。我们得出结论：WOGAN是自动生成测试生成器的可行方法，且这些测试生成器能为信息物理系统的运行时验证生成多个多样化的反例。