随着嵌入式系统在安全攸关领域的广泛应用，嵌入式系统的研究也逐步升温。由于混成系统既可以描述嵌入式系统离散的控制逻辑，又可以描述其连续的硬件行为，因此成为嵌入式系统理想的形式化模型。安全性验证问题是混成系统研究中最具挑战性的问题之一。由于混成系统中存在连续行为，离散系统的安全性验证方法无法应用到混成系统，这就要求人们研究针对混成系统安全性验证的方法。本文基于归纳不变式的方法研究混成系统安全性验证，分别从归纳条件的评价准则、归纳条件的定义以及归纳不变式的生成方法三个方面进行了研究。本论文的主要贡献如下：初步建立了一套形式化的混成系统归纳条件评价准则。该准则有助于理解归纳条件的本质特征，并指导建立更好的归纳条件和求解方法，为后面归纳不变式的研究奠定理论基础。提出了一种基于指数条件和半定规划的归纳不变式(称为屏障证书)生成方法。基于指数条件的归纳不变式可以为系统的可达集形成一个更加精确的过近似，因此可以验证非安全集合与可达集紧密的安全性属性；该条件还具有凸性，从而能够利用半定规划实现高效的不变式求解。提出了一种基于完备条件和量词消去的归纳不变式生成方法。相对于前一种方法，该方法具有完备性，从而拥有更大的验证能力。与已有的完备归纳条件相比，本文的完备归纳条件可以很容易地被改写，从而获得一簇具有不同保守性和计算复杂度的充分归纳条件，因此提供了一种在验证能力和计算复杂度之间进行权衡的手段。设计了基于量词消去和SMT的归纳不变式求解算法。实现了一个混成系统归纳不变式的生成工具HIIDiscoverer，能够有效地求解混成系统归纳不变式。