混合系统是连续动态过程和离散事件动态过程并存,且相互影响、相互作用的一类动态系统。八十年代后期,随着微型计算机、大型通讯网和微处理器在控制领域的大量应用,混合系统广泛出现于生产实际中,混合系统成为自动控制和计算机理论两大领域的研究热点。论文首先介绍了混合系统的概念和一些混合系统的典型实例,针对混合系统的建模、分析、验证方法作了系统的阐述。详细介绍了混合系统形式验证的研究现状、验证工具和基本概念。针对混合系统既包含连续动态过程又包含离散事件过程的特点,研究了通过混合自动机模型进行混合系统建模的方法;对于混合系统验证中的模型检验问题,分析了计算树逻辑CTL和基于动作的时序逻辑ACTL。对可达集的表示和计算方法进行了较为深入的研究:对比了使用凸多面体、超矩形和有向矩形壳表示可达集时,在过近似的保守性,计算的复杂度,集合交、并处理能力和维数增长时凸多面体顶点和面的增长速度等方面的优劣。在此基础上,归纳出了可达集的表示和计算方法的选用原则。流管道的近似方法是形式验证技术的一个重要内容。根据混合系统中的连续部分的动态特性,可将混合系统分为时钟型、线性和非线性三种类型。对于不同类型的混合系统,其流管道近似方法都不相同。本文针对这三种类型的混合系统,详细分析了各个类型混合系统的流管道近似方法,并分别对浓度控制系统(时钟型)、化工蒸发过程(非线性)和常压炉加热系统(线性)作为形式验证的对象,对它们的连续动态和离散动态部分分析的基础上,建立混合自动机模型,提出需要验证的形式规范,采用各自的流管道计算方法对可达集近似过近似,最后得到形式验证的结果。