基于符号-数值混合计算方法的复杂混成系统验证研究

Complex hybrid systems are large-scale nonlinear hybrid systems. Due to such feature, formal verification of complex hybrid systems has been one of the most important and challenging problems in computer science. In this project, we plan to resolve the formal verification problem of complex hybrid systems based on symbolic-numeric approach, from the perspective of computational methods. The key problems in this project are as follows: 1) to suggest a convex relaxation of non-negativity of multivariate polynomial, which can be used to transforming the verification problem into a semi-definite programming, 2) to propose an algorithm for computing exact real solutions of semi-definite programming, 3) to suggest a new algorithm for quantified nonlinear constraint solving, which can be used to generating invariants and Lyapunov functions for complex hybrid systems, and 4) to apply our method to verify the safety of the tlight collision avoidance maneuver. The research results will provide a powerful support for quality assuring of hybrid systems.

复杂混成系统是指规模较大、非线性程度较高的混成系统。复杂混成系统的这些特征使得其形式化验证非常困难。如何设计面向复杂混成系统的形式化验证方法一直是计算机科学领域的研究热点和难点。本项目围绕复杂混成系统验证开展研究工作，从计算方法的视角，针对单纯符号计算方法可扩展能力不足和单纯数值计算方法数值结果正确性无法保证等问题，研究基于符号-数值混合计算的形式化验证方法与技术：研究基于凸松弛的多元多项式非负性判定方法，从而将复杂混成系统的验证问题转为半正定规划问题；研究基于符号-数值混合计算的精确解计算方法，从而给出半正定规划问题的准确结果；在此基础上研究新的含量词的非线性约束求解技术，以支持基于不变式生成和Lyapunov函数构造的复杂混成系统安全性与活性验证；围绕空中交通管制系统中的飞行防撞策略开展相关验证技术的实例研究。本项目的研究将为混成系统的设计和质量保证提供方法和技术支撑。

本项目围绕复杂混成系统验证开展研究工作，针对现有验证技术在计算效率、可扩展性和可处理的系统类型等方面的不足，提出了基于符号-数值混合计算的形式化验证方法与技术：在非线性约束求解方面，构建了基于Krivine-Vasilescu-Handelman正点定理的线性松弛方法和基于迭代线性规划的双线性规划求解技术；建立了基于Krawczyk算子方法的非线性系统实根存在性判定方法，实现了区间多项式的非负性判定。在复杂混成系统验证方面，设计了面向多项式混成系统、非多项式混成系统、不确定混成系统、随机混成系统等的多种障碍函数构造算法，实现了不同类型混成系统安全性的快速验证；提出了基于线性规划的深度神经网络鲁棒性验证算法，取得了较好的验证效果和计算效率，可进一步应用于含智能组件的CPS系统验证。本项目的研究为混成系统的设计和质量保证提供了方法和技术支撑。