混合系统理论是控制工程理论与计算机科学验证交叉的学科领域。混合系统理论主要涉及到有限自动机表示的离散状态与微分方程表示的连续动态相互作用的建模、分析、控制和验证。为了了解混合系统的行为和验证混合系统是否在某种条件下能安全运行，需要先进的理论知识和分析工具。混合系统的形式验证是混合系统研究的一个重要领域，至今仍未出现比较成熟的方法体系，验证工具大部分都停留在实验室研究阶段，难以广泛适用于工业目标。在这种背景下，本文围绕混合系统的形式验证问题，以解决验证中连续动态计算所存在的困难为研究重点，其中又以可达集的计算为主要内容。针对流管道近似方法在非线性系统中存在的计算复杂性，给出了两种简化方法：变时间间隔的流管道近似方法和逼近法。逼近法指用流管道近似逼近切换面或者用多面体逼近切换面寻找某一时刻，在此时刻开始计算流管道近似凸多面体与切换面的交集。在对流管道近似方法进行分析的基础上，提出一种新的计算切换面上可达集的方法。用凸多面体包裹切换面上的实际可达集，利用优化算法求出包裹的最小凸多面体，而实际可达集的求取是通过对初始区域上某点，计算其对应于切换面上的点的数值解，将数值解嵌入优化算法中得到。这里给出的凸多面体是指在切换面子空间上的闭区域。论述了一种基于反例的状态划分方法，即仅针对与验证规范有关的状态进行划分，在一定程度上避免由于再划分整个状态空间导致的状态爆炸问题。在对反例状态的划分上，由于暂时无法精确划分状态使之与该状态的后续子状态相对应，给出了多次“对半”剖分的划分方法。经过多次地划分，这种“对半”剖分方法能够确定划分后的反例状态集合与后续子状态相对应。在实验部分，结合验证工具CheckMate对倒立摆模型进行了验证；利用线性切换系统的验证过程给出了反例划分的实验结果；在非线性跳跃小球系统的验证中，列出了文中提出的可达集计算与简化方法的实验结果，并与简化前的计算方法得到的实验结果进行了对比分析，阐述了改进方法的可行性。最后，对研究内容进行了总结，分析了工作成果的不足之处，并对今后的研究方向作了展望。