混合系统主要研究由连续性子系统和离散性子系统相互作用而构成的一类动态系统。连续性子系统和离散性子系统二者相互作用,使系统的运行轨迹整体上呈现离散状态的迁移,局部上呈现连续状态渐进演化,表现出更加复杂的动态行为,这就给混合系统运行的安全性和状态的可达性分析带来了困难。本文的工作是围绕线性混合系统的形式化验证展开的。线性系统具有初始区域为凸多面体且可达集仍为凸多面体的特性。混合系统不变集内的子系统为线性系统,因此可应用线性系统的特性对线性混合系统的形式验证过程进行简化。本文以炼油厂常减压装置中的常压炉加热系统为线性混合系统的例子,分别应用基于流管道和基于简化流管道的形式验证方法进行验证,为线性混合系统的形式验证提供参考。主要工作包括:1、研究了基于流管道理论的验证方法,包括:初始状态区域划分、流管道的过近似,商迁移系统迁移关系的确定。2、对目前主要的验证工具进行了比较,并详细分析了基于流管道理论的验证工具CheckMate各模块的功能。3、在详细分析了常压炉加热系统工作原理的基础上,建立动态模型,抽象其验证问题;建立混合自动机模型,应用基于流管道的形式验证方法对系统的状态可达性和运行安全性进行分析,得出验证结论;分析了在验证过程中采用不同步长对验证结果的影响。4、应用基于简化流管道的形式验证方法,对原油加热过程进行验证,对验证结果进行分析。并与基于流管道的形式验证方法得到的验证结果相比较,讨论了两种验证方法的计算复杂度和保守性问题。