混成系统是一类复杂的动力系统,其中既包含了连续演变行为又含有离散变迁行为,并且两者又交织发生.连续演变状态可用于描述各个独立物理硬件的连续行为,离散变迁状态可用于描述离散控制或不同模态切换行为.因此,使得混成系统能很好的应用于嵌入式系统及其逐步发展衍生的信息物理融合系统（即CPS）的形式化分析与建模研究之中.随着信息技术和制造工程的快速发展,嵌入式系统和CPS在众多关系国计民生的安全攸关领域,如航空航天、智能交通、医疗卫生等均有广泛应用.因而,结合数学与计算机方法研究混成系统安全问题已成为软件工程领域的热门而前沿的研究课题,具有重要的科学价值和实际意义.障碍函数生成方法作为混成系统安全验证主流方法之一,由于避免了对混成系统状态可达集计算的困难而广受关注.这类方法关键问题在于两方面,一方面,目前已有的障碍验证条件过于保守;另一方面,障碍验证条件求解模型计算复杂度高.对此,本文针对混成系统的障碍函数生成方法进行深入研究,分别从以下三个角度:创造新的低约束障碍验证条件、简化障碍函数生成模型计算、复杂系统模型抽象方法进一步降低障碍函数生成的计算复杂度进行研究.本论文的主要成果及贡献有以下几点:·提出新的障碍验证条件构造.本文是基于采用Darboux多项式特殊性质进行构造的一类障碍函数,称为Darboux型障碍函数生成.由于采用新的安全验证条件构造方式,因而能生成已有障碍验证方法所不能生成的障碍函数,通过实验结果也可说明这点.另外,得益于Darboux型障碍验证条件转化而来的问题模型的特殊特点,本文提出一个LS-QP交叉投影的求解方式,能非常高效的计算Darboux型障碍函数,实验结果能证明本文提出的算法具有高效性.·提出一种新的基于BMI模型求解的障碍函数生成方法.首先利用SOS松弛方法将经典的微分障碍函数验证模型转化为一类BMI约束求解模型.本文进一步针对一般化BMI约束求解问题进行研究,最终给出求解一般BMI约束问题的变向增广拉格朗日迭代方法（Alternating Direction Augmented Lagrangian Method）的显式表达式.将该结果用于障碍函数生成问题,并给出求解算法.与当前主流软件PENNON核心算法进行比较,本文求解算法复杂度更低.·提出新的系统抽象方法.针对复杂的非线性混成系统模型本身进行研究,提出线性抽象的构造方法,避免了通过直接求解复杂的原系统障碍验证所造成的高计算复杂度.将给定的非线性混成系统转化成相应的具有待定参数的线性抽象系统,接着对抽象得到的线性系统运用量词消去方法进行线性障碍验证生成,该线性混成系统的安全性同时保证了原系统的安全性.实验证明,本文提出的基于线性抽象的障碍函数生成,能解决原本直接利用量词消去不能解决的非线性系统安全问题.