混合系统是指嵌入于物理环境中的数字实时系统．由于计算机技术的快速发展，混合系统在各行各业中都得到广泛应用，但是由于混合系统涉及到连续时间，因此其验证问题始终没有得到完善的解决．近年来，人们普遍采用模型检验方法对混合系统进行验证．由于线性混合系统在实际应用中可以表示大多数的嵌入式实时系统，因此我们着重研究这类混合系统的验证算法．本文首先介绍了混合系统的模型—混合自动机，然后提出了一种针对线性混合系统的基于区域的先划分再遍历的半确定性验证方法．经实例检验，该方法能够有效地验证线性混合系统．最后将本文的方法同有关的其它算法进行了比较 Hybrid systems are digital real-time systems embedded in the physical environment. Due to the rapid development of computer technology, hybrid systems have been widely used in all walks of life. However, due to the continuous time involved in hybrid systems, the verification problem has not been completely solved. In recent years, people generally use the model test method to verify the hybrid system. Since linear hybrid systems can represent most of the embedded real-time systems in practice, we focus on the verification algorithms of such hybrid systems. In this paper, the hybrid system model-hybrid automaton is introduced firstly. Then a semi-deterministic method based on region-based prior recursive sub-traversal for linear mixed systems is proposed. The example test shows that this method can effectively verify the linear mixed system. Finally, the method in this paper is compared with other related algorithms