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

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..

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

混杂系统是一种应用广泛，行为复杂的信息系统。异步电路系统是一类特殊的混杂系统，这种系统取消了同步时钟的管理机制，而采用实现握手协议的通讯宏单元或多线复用的准延迟方式来协调和管理整个电路行为，这种特征导致异步电路更适合采用基于形式化混杂系统的方式来分析验证。.在 2015至2017年项目执行期，项目组主要针对异步集成电路这种典型和实用的混杂系统，在理论、工具和实践三个方面从模型层、方法层、行为层和验证层进行创新性研究。在理论研究方面，项目组研究了混杂系统建模、性质刻画与约束、分析验证方法三方面的内容；在工具研发方面，项目组研发了多套软硬件工具，（部分）实现了理论研究的成果；在实践研究方面，项目组根据理论研究成果，并借助相关软件工具，针对多类异步集成电路系统进行开发、验证与仿真。.在进行科研的同时，项目组积极培养研究生，资助研究生参加各类会议和培训，培养学生科研素养和能力；此外项目组老师也通过此项目的资助，通过会议、访问和联合研发的形式，巩固了与国内外学术界和生产单位的联系，加强了此项目的社会意义。.项目执行期内，项目组共发表学术论文16篇：EI检索3篇，SCI检索2篇，CPCI-S检索1篇，中文核心3篇，待检索7篇；参与译著1部；申请发明专利5项；申请实用新型专利1项（已授权）；获得省部级科技进步二等奖1项，其他奖励2项。已培养硕士研究生15名，已毕业8名，其中攻读博士3人。