随着计算机算力的快速提升以及大量数据的驱动,以神经网络为代表的深度学习（Deep Learning,DL）技术在许多领域取得了长足的进步。因此,神经网络也越来越多的被应用于自动驾驶等安全相关领域,而如何确保这样的系统的安全性也成为人们越来越关注的方向。与此同时,在对神经网络的研究中人们发现,神经网络容易受到一些人为精心设计的样本的欺骗。这些样本与原始的输入样本仅有很微小的差别,人类几乎无法分辨,但是却能使神经网络的分类出错。因此,以研究如何快速有效地生成这样的样本为目标的对抗学习（Adversarial Learning）成为近年来机器学习领域的一个热点。然而,就对抗学习领域而言,目前主流的研究方向均为如何使得神经网络分类出错,却忽略了这些错误在系统层级的语义信息。明确在何种场景下,神经网络的分类错误会对系统安全产生严重威胁,是对智能系统进行安全保障和加固的必要前提。形式化方法采用严格的数理逻辑证明来构建软件和硬件系统。由于其具有较高的严谨性,该方法已被广泛运用到系统级别性质验证的研究中。其中,模型检测技术被广泛用于分析并验证一个系统是否满足安全性等性质。基于这样的思想,本文以含有神经网络的安全攸关系统（AI Powered Safety-Critical System）为研究对象,使用了模型检测的方法检测一个安全攸关的系统中,神经网络的哪些分类可能导致系统不满足安全性。根据这些分类,对输入样本进行定向攻击,生成一些对系统安全产生实际威胁的对抗样本。本文根据上述技术路线,基于自动驾驶场景进行了实验探究,实验结果表明本文所提出的方法在生成系统级别对抗样本时相较于传统的方法具有更高的效率。本文主要贡献如下:·提出了含有深度学习组件的系统的建模方法。以含有神经网络的安全攸关系统为例,给出了含有深度学习组件的安全攸关系统的建模方法。首先对神经网络的输出进行分析,判断其可能的所有情况,再对整个系统进行合理的建模,其根据神经网络的分类结果进行决策。然后,通过模型检测的方法,判断神经网络的哪些分类可能使得系统不满足安全性质。·提出了面向系统功能安全的对抗样本生成算法。基于模型检测结果,对神经网络对应的输出节点求前向导数,并计算显著性图。根据显著性图最大值,找到对应的输入特征,并迭代地对其进行扰动,生成面向系统功能安全的对抗样本。·基于具体场景进行了案例探究。对自动驾驶场景下含有神经网络组件的安全攸关系统进行建模,检测出神经网络的何种输出可能导致系统层级错误。基于模型检测结果,生成系统级别的对抗样本,并与传统对抗攻击方法进行对比,展示了基于模型检测的对抗攻击的可行性和有效性。