在混合系统中,离散事件和连续动态行为相互作用的特性使得系统开发的正确性难以保证,尤其对于安全悠关的系统,如电力系统和化工系统,错误运行将造成重大损失。而形式验证的目的在于检验混合系统是否在任何环境下都能安全运行。混合系统的形式验证是混合系统研究的一个热点和难点,至今仍未出现比较成熟的方法体系,验证工具大部分停留在实验室研究阶段,距离能够广泛适用于工业界的目标仍有相当远的距离。 本文所有论述均围绕着解决混合系统的形式验证问题这个主题展开,主要工作有: 1.在国内混合系统的形式验证研究刚刚起步的情况下,通过大量的国内外文献阅读,对各种基于模型检验的混合系统形式验证方法进行了整理和总结,归纳出基于模型检验的混合系统形式验证原理,包括可达集的计算、商迁移系统、仿真对和混合系统形式验证的过程,并对目前主要的验证工具进行了分析和比较。 2.研究了基于流管道和切换面划分的混合系统形式验证方法:在研究多面体不变集混合自动机和离散抽象迁移系统概念的基础上,分析了有限状态近似商迁移系统的计算方法,包括阈值切换面划分、迁移系统状态的确定、流管道计算和迁移关系的确定。 3.当系统为线性定常连续动态并且初始区域为凸集时,针对连续动态流管道计算的困难,提出有关系统演化轨迹规律的具体结论并加以证明,依据这些结论对商迁移系统中迁移关系的计算方法进行了改进,改进的迁移关系计算将节省大量的计算时间和计算量。 4.根据一个倒立摆实例及其控制规范要求,给出了适用于验证工具CheckMate的系统描述和规范描述,应用验证工具对倒立摆模型进行了验证,并给出验证结果。