采样控制系统的安全性验证方法及其应用

Existing approaches for safety verification of hybrid systems lack applicability, scalability and usability. In order to improve the efficiency of safety verification for sampled-data control systems, a special class of hybrid system, the proposed project plans to investigate new verification scheme that combines existing approaches based on reachable set computation and invariant generation, to promote the precision and efficiency of continuous-time reachable set computation, to design more efficient algorithms for solving polynomial constraints derived from invariant generation, and to develop tools for case studies in the fields of spacecraft control and battery management. By extending Taylor-model based reachable set computation we bridge the gap between the reachable set computation and invariant generation methods, by proposing strategies for local error analysis and self-adaptive step-size adjustment as well as non-polynomial system abstraction we gain higher precision and efficiency in reachable set computation, by applying interval arithmetic and interval constraint propagation as well as linear inequality transformation over bounded region we obtain more efficient polynomial constraint solving algorithms. The final goal of this project is to establish a new verification approach for safety verification of sampled-data control systems and carry out fruitful practical applications. The research conducted in this project will strongly advance the development of the hybrid system verification area, and will be of great significance for enhancing the trustworthiness of safety-critical embedded control systems.

本项目针对现有混成系统安全性验证算法存在缺乏普适性、可扩展性以及易用性的问题，以提升采样控制系统这一特定混成系统安全性验证效率为目标，拟开展针对采样控制系统的可达集计算和不变式生成相结合的新型验证方法研究，连续系统可达集计算精度和效率提升研究，面向不变式生成的高效多项式约束求解算法研究，验证工具研制及其在航天器轨道姿态控制、新能源汽车动力电池管理等领域的应用实例研究。通过拓展连续系统可达集的泰勒模型解法实现可达集计算和不变式生成方法的嫁接，通过提出局部误差分析、自适应步长调节及非多项式系统抽象等策略提升可达集计算精度和效率，通过区间算术、区间传播技术和线性区间不等式转化实现有界域上多项式约束求解的高效算法，从而最终建立一种采样控制系统验证的新的高效方法并开展富有成效的实际应用。本项目的研究将有力推动混成系统形式化验证方向的发展，对保障安全攸关嵌入式控制系统的可信性有重要意义。

混成系统是包含状态连续变迁和离散跳跃的系统，是嵌入式控制系统的理想模型，混成系统的形式化验证和控制器设计研究对于保障安全攸关嵌入式系统的可靠性具有重要意义。本项目创新性地将机器学习技术和形式化验证技术相结合，首次提出了基于神经网络的数据驱动的连续和混成系统不变式（障碍函数）生成方法、可达集计算方法以及安全控制器生成方法，开发了相应工具，开展了一系列实例研究，展现了所提方法的高效、普适、易用性。.1. 基于神经网络的不变式（障碍函数）生成：提出用神经网络表示连续和混成系统的障碍函数安全凭证，通过设计合理的神经网络架构、训练数据产生方式、训练损失函数等，构建了神经网络障碍函数的自动生成框架，同时结合形式化后验证策略保证所得障碍函数的严格性；利用所开发工具nnbarrier进行了实例研究，结果表明本方法表示能力强、生成可能大、适用范围广。.2. 基于神经网络的可达集计算：提出用神经网络表示连续系统的可达状态集，即构建以系统初始集和时间为输入的神经网络，然后训练神经网络使其导数逼近连续系统微分方程的右端项，以此逼近系统的可达集；开发了工具nnreach，实例研究表明本方法可借助神经网络的强大表达能力提高可达集近似精度。.3. 基于神经网络的安全控制器生成：提出用神经网络同时表示系统的控制器和系统安全性的障碍函数凭证，通过训练同时学得控制器网络和障碍函数网络，结合形式化后验证保证了控制器的严格安全性，实现了“验证在环设计”；通过进一步优化损失函数改进了控制器的渐近稳定性等性质；开发了工具nncontroller，实例研究表明本方法适用范围广、人工干预少、所得控制器结构简单。.本项目基于上述成果共发表学术论文4篇，包括CCF B类（HSCC 2020，CPS领域旗舰会议）和C类（ICFEM 2019）推荐会议论文各1篇。项目实施过程中开展了同美国新墨西哥大学、英国约克大学等高校的国际学术交流，参加HSCC 2020和SETTA 2020国际学术会议并作分组报告，参加国内CCF ChinaSoft 2020大会并作YR-FMAC分论坛学术报告。本项目研究成果有望在自动驾驶、机器人等安全攸关智能控制系统领域取得应用。