本项目研究混合系统的可靠性和安全性验证技术。研究约束凸多面体结构表示和处理矩形混合系统的无穷状态空间；以该结构为基础，研究矩形混合系统的可达状态集计算算法和模型检测规则，从而建立矩形混合系统完整的自动验证理论和算法；研究近似转换算法把线性和非线性混合系统转换为矩形混合系统进行间接验证。.研究成果：(1) 构建了PLTL公式到非确定性自动机的转换算法，建立了扩展区间时序逻辑的统一模型检测规则和投影时序逻辑的完备公理系统，从而建立了离散状态系统的验证理论；(2) 构建了一种约束凸多面体模型和一种多速率图表的数据结构表示和处理多速率混合系统的无穷状态空间,建立了多速率混合系统基于稠密的时间区间时序逻辑的模型检测算法；(3) 通过对混合区域放开不等式约束条件进行扩展，建立了非初始化的矩形混合系统的无穷状态空间搜索模型；定义了一种称作矩形图表的数据结构表示扩展的混合区域的并，来降低非初始化的矩形混合系统可达性分析的算法复杂度；(4) 通过构造两种类型的模型检测操作，建立了矩形混合系统基于全部的时间计算树逻辑公式的模型检测算法，通过转换为实时系统基于区间时序逻辑的模型检测问题，解决了矩形混合系统基于混合时序逻辑的模型检测问题；(5) 通过构建非线性空间的闭包矩形，给出了非线性混合系统到矩形混合系统的一个近似转换算法进行近似验证；(6) 作为验证问题的扩展和应用场景，对工作流、UML序列图的可靠性验证、多核调度算法及验证等问题展开了研究，并取得的大量的研究成果。