We present the OGAN algorithm for automatic requirement falsification of cyber-physical systems. System inputs and output are represented as piecewise constant signals over time while requirements are expressed in signal temporal logic. OGAN can find inputs that are counterexamples for the safety of a system revealing design, software, or hardware defects before the system is taken into operation. The OGAN algorithm works by training a generative machine learning model to produce such counterexamples. It executes tests atomically and does not require any previous model of the system under test. We evaluate OGAN using the ARCH-COMP benchmark problems, and the experimental results show that generative models are a viable method for requirement falsification. OGAN can be applied to new systems with little effort, has few requirements for the system under test, and exhibits state-of-the-art CPS falsification efficiency and effectiveness.

翻译：我们提出OGAN算法，用于自动反驳网络物理系统的需求。系统输入和输出被表示为随时间变化的分段常数信号，而需求则用时序逻辑公式表述。OGAN能够发现导致系统违反安全性的输入反例，从而在系统投入运行前揭示设计、软件或硬件缺陷。该算法通过训练生成式机器学习模型来产生此类反例，以原子方式执行测试，且无需被测试系统的任何先验模型。我们利用ARCH-COMP基准问题对OGAN进行评估，实验结果表明生成式模型是实现需求反驳的可行方法。OGAN可轻松应用于新系统，对被测系统要求极低，并展现出最先进的CPS反驳效率与有效性。