深度神经网络在许多复杂应用场景中证明了其替代人类智能进行决策的潜力。信息物理融合系统中大量嵌入了深度神经网络控制器进行智能控制。深度神经网络黑箱本质、神经元数量大和非线性的特征,使得对其行为进行理解和分析非常困难。特别的,如何确保深度神经网络控制的安全攸关系统满足必须的安全性质,成为迫切而又极具挑战的难题。基于混成系统为安全攸关信息物理系统建模,运用形式化验证技术分析验证系统的行为是否满足安全性质,是保障这类系统安全性最有效的手段。针对深度神经网络控制的混成系统,已有的工作通过计算可达集和基于数据驱动的方法构造栅栏函数来验证系统的安全性质。计算可达集验证系统的安全性仅能保证有限时间内的系统安全。基于数据驱动的栅栏函数构造方法受样本数据的影响大,面向高纬度系统时,成功率不高。针对上述问题,本文首次提出了两种新型栅栏函数构造方法来验证深度神经网络控制混成系统的安全性。与数据驱动的方法不同,这两种方法分别通过构造近似系统和逼近系统,直接生成待验证系统的栅栏函数,具有更高的成功率。具体的,本文的主要研究工作如下:1首次提出一种新的基于多项式近似系统的栅栏函数生成方法。其核心思想在于使用多项式逼近DNN控制器,并基于系统真实运行轨迹评估两者之间误差,从而将原本复杂的DNN控制器转化为带误差的多项式控制器,以此构造近似的半代数混成系统来生成原系统的候补栅栏函数。随后运用SMT求解器从这些候选栅栏函数中选出真正的栅栏函数。为克服近似误差带来的副作用,进一步设计了迭代框架,通过适度扩展误差估计上界,提高生成的成功率。相比于已有的基于仿真的候补栅栏函数生成方式,该算法更加稳定高效。2首次提出基于逼近系统的栅栏函数生成方法。数据驱动的栅栏函数生成方法受限于后端SMT求解器的验证能力,对一些高维系统和高复杂度的控制器无法在有限时间内验证,因此本文又提出一种栅栏函数的直接生成方法。该方法引入伯恩斯坦多项式抽象来构造抽象半代数系统,同时利用伯恩斯坦的泛化定理得到逼近多项式和原神经网络控制器间误差的严格上界,保证生成的抽象半代数系统是原系统的严格闭包,这也意味着该抽象半代数系统的栅栏函数一定也是原系统的栅栏函数而不必再经过SMT求解器验证。为了缓解伯恩斯坦多项式逼近误差较大的问题,本文进一步提出了一种基于划分的迭代式验证框架,能够有效的将原问题转化为多个子问题从而降低计算复杂度。该算法突破了数据驱动栅栏函数生成算法的计算瓶颈,大大扩展了可验证系统规模。3开发原型工具并完成对比实验基于以上工作,本文设计并实现了原型工具,在一组benchmark上评估了两种算法的有效性,并与当前先进的工作进行对比。实验证明,相比已有工作,本文提出的两种方法在栅栏函数生成成功率和可处理问题的规模上有显著提升。