基于可满足性模理论的混杂系统层次化分析验证技术研究

项目名称： 基于可满足性模理论的混杂系统层次化分析验证技术研究

项目编号： No.61402121

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 何安平

作者单位： 广西民族大学

项目金额： 24万元

中文摘要： 随着系统的信息化程度日益提升，系统行为的复杂度越来越高，如何有效保证系统设计的正确性，成为计算机科学领域研究的热点问题之一。由于系统超高的复杂性，传统的测试和仿真检验技术的缺陷越来越大，形式化分析验证方法成为保障正确系统的重要环节。 本项目研究一种有效和实用的混杂系统形式化分析验证理技术，分为三部分：（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.

英文关键词： semi-algebra based hybrid automata；hierarchical frame of design and analysis；satisfiable module theory；formal verification；asynchronous circuit