混合系统是连续变量过程和离散事件过程并存，且相互交换信息的一类动态系统。八十年代后期，随着微型计算机、大型通讯网和微处理器在控制领域的大量应用，一批反映先进技术发展方向的人造系统大量涌现，连续动态过程与离散事件混合的系统广泛出现于生产实际中，混合系统成为自动控制和计算机理论两大领域的研究热点。论文首先回顾了混合系统的产生背景，介绍了混合系统的概念、特点、研究意义及发展现状，重点介绍了混合系统的形式化验证方法，分析了系统仿真与形式化验证的异同，对现有的基于模型检验的混合系统形式化验证工具进行了对比与分析。针对混合系统既包含连续动态过程又包含离散事件过程的特点，研究了通过混合自动机模型进行混合系统建模的方法；对于混合系统验证中的模型检验问题，分析了计算树逻辑CTL和基于动作的时序逻辑ACTL。对可达集的表示和计算方法进行了较为深入的研究：对比了使用凸多面体、超矩形和有向矩形壳表示可达集时，在过近似的保守性，计算的复杂度，集合交、并处理能力和维数增长时凸多面体顶点和面的增长速度等方面的优劣。在此基础上，归纳出了可达集的表示和计算方法的选用原则。研究了基于可达集近似和切换面划分的混合系统验证方法，包括：初始划分、可达集近似、迁移关系的确定以及当出现不可决策状况时的细划分等。提出了通过顶点仿真与可达集近似相结合的迁移关系简化算法：针对线性定常系统的特点，结合凸多面体的性质，给出了在连续状态方程为线性定常的不变集内，当初始区域为凸多面体时系统可达集的演化规律，并加以证明。依据这些结论，对混合系统形式验证中迁移关系的计算方法进行了简化，并给出了计算过程与程序实现框图。根据文中提出的方法，结合实例编写了验证程序，实现了验证过程。并在计算量和保守性两方面将两种方法进行了详细的分析对比。分析结果表明：用简化后的算法计算商迁移系统的迁移关系，在保持计算效果的基础上，不但减少了系统过近似的保守性，而且仅需要少量的流管道计算，就能求出系统的迁移关系。最后，在对全文的研究工作进行了总结的基础上，对今后的研究方向作了展望。