混杂系统的形式验证技术是利用数学分析方法对混杂系统的安全性进行验证。近十年来,模型验证技术是形式验证研究的主要方法。模型验证技术是指,利用计算机强大的计算功能自动地对混杂系统的数学模型进行整个状态空间中进行遍历搜索,对系统所有可能的运行轨迹进行收敛计算或过近似计算,以检验系统的实现方案是否满足系统的设计要求。论文首先介绍了模型验证的概念和特点,常用的混杂系统建模方法如混杂自动机、混杂Petri网、层次结构和时段演算。分析了可达集的两种计算方法—前向和后向可达集算法,对可达集的过近似方法作了系统的阐述。最后详细介绍了模型验证的国内外研究状况和常用的模型验证工具。针对混杂系统连续子系统和离散子系统相互作用的特点,研究了混杂自动机模、多面体混杂自动机和混杂I/O自动机的建模方法;对于混杂系统的流管道过近似问题,给出了齐诺多面体(zonotopes)的基于中心点和生成元(generators)的表达式和过近似算法,分析了该算法的保守性、封闭性、集合交并处理能力以及收敛性。通过比较凸多面体过近似和齐诺多面体过近似算法的适用对象、计算方法、过近似保守性和随维数增长的计算复杂度,对两种算法的优劣和特点进行了详细的分析。针对常压炉加热炉系统(线性混杂系统)和汽车自适应巡航系统(非线性混杂系统)建立数学模型,抽象出验证问题,给出ACTL验证规范。使用PHAVer和CheckMate验证工具分别对上述两种系统建立混杂I/O自动机模型和阈值切换系统模型,应用齐诺多面体流管道过近似方法和凸多面体流管道过近似方法进行模型检验,对系统的状态可达性和运行安全性进行了分析,并给出验证结论。通过上述结论,分析验证工具CheckMate和PHAVer的保守性、消耗时间和内存空间占用率,对上述两种验证工具的验证效果进行了比较。