混杂系统是连续变量动态系统和离散事件动态系统相结合，并且二者相互影响相互作用的一类系统。混杂系统形式验证是混杂系统的一个研究方向，它是分析在给定的初始条件下，系统的可达集是否都在目标状态集合内。形式验证的目的是检验混杂系统是否在任何环境下都能安全运行。如今混杂系统的形式验证已经成为混杂系统研究的一个热点和难点。　　 混杂系统形式验证中计算可达集是重要的一步，选用何种可达集表示法对整个验证的精度有重要影响。本文所有的论述均围绕混杂系统形式验证中可达集计算这个主题展开，主要工作有：　　 1.通过大量的国内外文献阅读，对混杂系统形式验证方法进行整理和总结，对形式验证中可达集分析方法进行归纳，对现阶段混杂系统形式验证的主要问题进行总结。　　 2.在介绍混杂系统形式验证基本概念的基础上对可达集表示法中的有向矩形壳和凸多面体法进行了较为深入的研究。提出了新的可达集表示方法—有向凸多面体法，这种表示法的特点是以上两种可达集表示法的折中。通过样本点实验分析了三种表示法的计算复杂度，对三种表示法构造的几何体顶点数和面数进行比较。　　 3.总结了流管道保守性判定方法—观察比较法和误差比较法，针对误差比较法的缺点进行了改进。在此基础上提出了新的流管道保守性判定方法—体积比较法。给出了有向矩形壳和凸多面体混合算法的思想并且在已有的流管道保守性判定方法基础上给出了具体的算法。　　 4.根据文中提出的有向凸多面体法算法和有向矩形壳和凸多面体混合算法，结合一个非线性分段系统实例编写了验证程序，实现了验证过程。并在计算量和保守性两方面进行了详细的分析比较。分析结果表明：利用文中提出的两算法在验证过程中能够更好地在计算量和保守性两方面达到折中。　　 5.在对全文研究工作进行总结的基础上，对今后的研究方向作了展望。