在现代流程工业中,过程控制对象日益复杂以及对控制精度的要求日益提高,工业过程控制中连续过程动态和离散事件动态的混杂特性越来越明显,传统的理论方法对这些系统进行建模和控制,已很难满足控制要求。针对这种情况,本文采用混合逻辑动态(Mixed Logical Dynamical,MLD)模型理论,进行混杂系统的建模、控制与形式验证研究。本文在前人研究工作的基础上,对混杂系统理论作了进一步的研究和探索。研究的内容包括基于MLD的混杂系统控制和形式验证研究两个部分,主要体现在以下几个方面:深入研究了混合逻辑动态系统建模机理,讨论了逻辑命题的转换及其线性整数规划的方法,分别以机理建模和Hysdel方法建立了CSTR系统的MLD模型,总结了混杂系统不同模型之间的等价性。将传统的模型预测控制应用到基于MLD模型的混杂系统中,研究了混合逻辑动态系统的开环约束最优控制,分别探讨了基于MIQP和MILP问题的模型预测控制,通过数值仿真验证了两种算法的有效性。探讨了定理证明和模型检验两种混杂系统形式验证方法,详细介绍了基于模型检验的形式验证工具,利用CheckMate验证工具对弹跳球系统进行了形式验证的仿真研究。研究了混合逻辑动态系统的形式验证问题,针对混合逻辑动态系统,在理论上深入研究了基于数学规划的混杂系统形式验证算法,将该算法应用到非线性CSTR系统中,探讨了CSTR系统的安全性问题,对混杂系统控制的正确性和可靠性进行了有益的探索。最后,对全文工作进行了总结,对混杂系统控制及形式验证技术未来的发展方向做了展望。