随着系统的信息化程度日益提升，系统行为的复杂度越来越高，如何有效保证系统设计的正确性，成为计算机科学领域研究的热点问题之一。由于系统超高的复杂性，传统的测试和仿真检验技术的缺陷越来越大，形式化分析验证方法成为保障正确系统的重要环节。.本项目研究一种有效和实用的混杂系统形式化分析验证理技术，分为三部分：（1）以实际混杂系统设计中最常采用的层次化设计方案为建模依据，使用多类别逻辑公式准确和快速地描述层次化设计模式，研究多类别逻辑公式到混杂自动机的转换方法；用时间计算树逻辑描述系统需求。（2）研究时间计算树逻辑公式与多项式近似混杂自动机误差间的关系，建立误差可控的混杂自动机近似技术。（3）研发多项式理论下的可满足性模理论（SMT）求解器，开发基于此SMT的混杂系统模型检测工具。第（1）和（3）项内容保证了本项目形式化模型和检测技术的实用性，第（2）和（3）项研究内容确保了项目的整体框架的有效性。

System behaviors become more and more complex, since the information technologies are deeply applied to these hybrid systems. The scientists in Computer Since region have been trying their best to find feasible ways to guarantee the correction of systems. The high complexity almost makes every traditional testing and emulating technologies fail, they found formal methods for this type of systems be very useful..In this project, we try to study an effect and feasible way of formal methods for modeling, verifying and analyzing the hybrid system. The contents include the following three parts: (1) According to the real hybrid system design, we try to adopt many-sorted logic to interpret the hierarchical module of the hybrid system, and then translate the formulas into hybrid automata, as well as the LCTL for system requirement as usual. (2) By studying the relation between the LCTL formulas and the deviation of the approximations of hybrid automata, we try to propose a polynomial based deviation-controllable way of approximation theory for hybrid automata. (3) With the polynomial theory of SMT, we try to build a model checker for polynomial hybrid automata. We think that (1) and (3) make our formal model and checking procedure feasible, meanwhile, the (2) and (3) show the effectiveness of the whole framework..