FalsifAI: Falsification of AI-Enabled Hybrid Control Systems Guided by Time-Aware Coverage Criteria
FalsifAI: Falsification of AI-Enabled Hybrid Control Systems Guided by Time-Aware Coverage Criteria
复制标题
DOI：
10.1109/tse.2022.3194640
复制
发表时间：
2023-04
影响因子：
7.4
通讯作者：
Zhenya Zhang;Deyun Lyu;Paolo Arcaini;L. Ma;I. Hasuo;Jianjun Zhao
中科院分区：
文献类型：
--
作者：
Zhenya Zhang;Deyun Lyu;Paolo Arcaini;L. Ma;I. Hasuo;Jianjun Zhao
需要执行复杂控制任务（例如自主驾驶）的现代网络物理系统（CPSS）越来越多地使用启用AI的控制器，主要基于深神经网络（DNNS）。这种类型的系统的质量保证至关重要。但是，由于它们的复杂性和无法解释的决策逻辑，他们的验证可能极具挑战性。伪造是一种既定的CPS质量保证方法，而不是试图证明系统正确性，而是旨在寻找一个时间变化的输入信号，违反了描述所需行为的正式规范；它通常采用一种基于搜索的测试方法，该方法试图最大程度地减少其定量语义给出的规范的鲁棒性。但是，鲁棒性提供的指导主要是黑框，仅与系统输出有关，但不允许了解是否已经充分探索了由多个连续执行神经网络控制器确定的时间内部行为。为了弥合这一差距，在本文中，我们尽早尝试探索由混合控制系统中的神经网络控制器的重复执行确定的时间行为，并首先提出了八个时间吸引的覆盖范围标准，专门为神经网络控制器设计而设计。 CP的上下文通过设计考虑不同的特征：神经元的简单时间激活，在给定持续时间内的神经元的连续激活以及随时间推移的差异神经元激活行为。其次，我们引入了一个伪造框架，名为$ \ mathtt {falsifai} $ falsifai，该框架利用了覆盖范围信息以获得更好的伪造指导。也就是说，在鲁棒性最小化的利用阶段，将增加覆盖率的控制器的输入（因此改善了DNN行为的探索）。我们对总共3个典型CPS任务，6个系统规格，18个DNN模型和12,000多个实验的大规模评估证明了1）我们提出的技术在表现优于两种先进的伪造方法的优势，即2）我们提出的时间感知覆盖标准的有效伪造指导的有用性。
Modern Cyber-Physical Systems (CPSs) that need to perform complex control tasks (e.g., autonomous driving) are increasingly using AI-enabled controllers, mainly based on deep neural networks (DNNs). The quality assurance of such types of systems is of vital importance. However, their verification can be extremely challenging, due to their complexity and uninterpretable decision logic. Falsification is an established approach for CPS quality assurance, which, instead of attempting to prove the system correctness, aims at finding a time-variant input signal violating a formal specification describing the desired behavior; it often employs a search-based testing approach that tries to minimize the robustness of the specification, given by its quantitative semantics. However, guidance provided by robustness is mostly black-box and only related to the system output, but does not allow to understand whether the temporal internal behavior determined by multiple consecutive executions of the neural network controller has been explored sufficiently. To bridge this gap, in this paper, we make an early attempt at exploring the temporal behavior determined by the repeated executions of the neural network controllers in hybrid control systems and first propose eight time-aware coverage criteria specifically designed for neural network controllers in the context of CPS, which consider different features by design: the simple temporal activation of a neuron, the continuous activation of a neuron for a given duration, and the differential neuron activation behavior over time. Second, we introduce a falsification framework, named $\mathtt {FalsifAI}$FalsifAI, that exploits the coverage information for better falsification guidance. Namely, inputs of the controller that increase the coverage (so improving the exploration of the DNN behaviors), are prioritized in the exploitation phase of robustness minimization. Our large-scale evaluation over a total of 3 typical CPS tasks, 6 system specifications, 18 DNN models and more than 12,000 experiment runs, demonstrates 1) the advantage of our proposed technique in outperforming two state-of-the-art falsification approaches, and 2) the usefulness of our proposed time-aware coverage criteria for effective falsification guidance.