混合系统是连续动态与离散动态并存且相互交互的异构动态系统。混合系统的应用非常广泛，如嵌入式系统、网络控制系统、工业制造、化学过程、航空交通控制等领域。混合系统的研究是将连续动态和离散过程混合在一起，考虑连续动态与离散动态的相互作用。因此混合系统不是单纯地从连续动态的角度进行研究，也不是单纯地从离散逻辑的角度进行研究，混合系统的理论体现了计算机科学与控制理论的交叉。 在混合系统的理论研究中，安全性问题一直是研究的热点，是询问给定初始条件和扰动，系统的所有运行是否会出现不安全的操作。安全性验证与安全性控制是安全性问题研究中密不可分的两个侧面。混合系统安全性的形式化验证是基于数学理论来严格地验证系统所有的行为满足系统性能规范。而安全性控制问题是设计一个离散事件监控控制器，使得混合系统在此控制器的控制作用下，其动态行为能够满足安全性要求。 由于混合系统的动态复杂性，安全性验证与控制问题是难解的，现有阶段的研究是基于抽象近似的方法，寻找问题求解的充分条件。 本文从计算机科学理论的研究角度对混合系统的安全性问题展开研究与探讨。本文分为两大部分：混合系统的安全性验证研究与混合系统的DES控制研究，从模型抽象约简及精化的角度深入研究了两个方面的问题。第一部分侧重于混合系统安全性验证的研究。重点研究了基于phase—portrait近似方法的安全性验证。Phase—portrait近似是通过模型转换的方法将复杂的混合动态系统转换为可判定的(或可计算的)混合自动机，主要贡献为： (1)在现有的文献中，Phase—portrait近似仅限线性Phase—portrait近似的应用，本文将线性Phase—portrait近似推广到多项式Phase—portrait近似，提出基于泰勒公式余项实现模态空间的划分；针对抽象模型的精化问题，提出通过增加多项式阶数来实现模型的逐步精化，并将动态误差加入模型的不变集阈值控制中，以动态跟踪近似误差，实现模型的精化调整。从理论角度证明了所述方法的正确性，并通过实例仿真比较了多项式Phase—portrait近似与线性Phase—portrait近似及精化调整的近似效果，表明了多项式Phase—portrait近似的可行性及有效性。 (2)phase—portrait近似的关键是控制模态状态空间的划分，目前的phase—portrait近似方法缺乏对模型空间划分策略的研究，现有的划分策略是均匀矩形式划分，这种均匀静态划分在模型精化过程中往往会引起模态数量的剧增。针对这一问题，本文提出了基于定性推理的phase—portrait近似，依据系统的动态特征来指导状态空间的划分及抽象模型的精化，提出了基于向量场特性及感兴趣多项式的李导数实现模态空间的划分，并通过多项式的高阶李导数实现模型的精化。从理论角度证明了所述方法的正确性，并通过实验比较了均匀矩形划分与定性推理划分对验证复杂性的影响，表明了基于定性推理模态划分验证的有效性。 第二部分侧重于混合系统DES监控控制的研究。混合系统DES控制的关键是混合系统的离散化，本文借鉴在混合系统安全性验证领域中模型的抽象精化方法，将之推广到混合系统的DES模型的抽象精化中，主要贡献为： (1)目前混合系统的DES监控框架中的DES受控系统具有模型过于抽象粗糙，且无法实现动态精化等缺点，往往无法满足控制分析的需要。针对这一问题，本文首次提出了混合系统的抽象DES对策模型概念，给出了一种基于混合系统的DES受控系统的DES对策模型构建方法，从而可以将搏弈论引入到系统的控制分析应用中。研究的进一步重点放在抽象DES对策模型的动态精化调整，以适合控制分析的需要。本文给出了基于对策互模拟过程(S—BisimulationProcedure，SBP)构造混合系统对策互模拟器的具体过程。借鉴混合系统安全验证中基于互模拟过程的抽象，提出了基于SBP的抽象控制，并使用局部调整策略来降低调整精化过程的复杂性，实现了根据控制分析的需要DES对策模型的动态精化。实现结果表明了基于SBP控制分析的有效性。 (2)抽象模型的精化往往会引起状态空间爆炸问题。在混合系统安全性验证中，基于反例的抽象精化是根据伪反例对抽象模型做局部的调整精化，是一种惰性精化过程，有效地预防了由于精化所引起状态空间爆炸问题。本文将这种方法推广到混合系统的DES对策模型的抽象精化中，不同于验证问题的反例，控制反例是图形结构，提出了基于反例图的抽象精化控制。给出了DES对策模型控制反例的分析方法及依据反例的模型调整过程，实现了DES对策模型的局部惰性精化调整。实现结果表明了基于反例控制分析的有效性。