基于障碍函数生成的混成系统安全验证研究

发布时间：2018-02-20 15:38

本文关键词： 混成系统安全性验证障碍验证生成符号计算达布多项式双线性矩阵不等式抽象解释多项式优化　出处：《华东师范大学》2017年博士论文　论文类型：学位论文

【摘要】：混成系统是一类复杂的动力系统,其中既包含了连续演变行为又含有离散变迁行为,并且两者又交织发生.连续演变状态可用于描述各个独立物理硬件的连续行为,离散变迁状态可用于描述离散控制或不同模态切换行为.因此,使得混成系统能很好的应用于嵌入式系统及其逐步发展衍生的信息物理融合系统(即CPS)的形式化分析与建模研究之中.随着信息技术和制造工程的快速发展,嵌入式系统和CPS在众多关系国计民生的安全攸关领域,如航空航天、智能交通、医疗卫生等均有广泛应用.因而,结合数学与计算机方法研究混成系统安全问题已成为软件工程领域的热门而前沿的研究课题,具有重要的科学价值和实际意义.障碍函数生成方法作为混成系统安全验证主流方法之一,由于避免了对混成系统状态可达集计算的困难而广受关注.这类方法关键问题在于两方面,一方面,目前已有的障碍验证条件过于保守;另一方面,障碍验证条件求解模型计算复杂度高.对此,本文针对混成系统的障碍函数生成方法进行深入研究,分别从以下三个角度:创造新的低约束障碍验证条件、简化障碍函数生成模型计算、复杂系统模型抽象方法进一步降低障碍函数生成的计算复杂度进行研究.本论文的主要成果及贡献有以下几点:·提出新的障碍验证条件构造.本文是基于采用Darboux多项式特殊性质进行构造的一类障碍函数,称为Darboux型障碍函数生成.由于采用新的安全验证条件构造方式,因而能生成已有障碍验证方法所不能生成的障碍函数,通过实验结果也可说明这点.另外,得益于Darboux型障碍验证条件转化而来的问题模型的特殊特点,本文提出一个LS-QP交叉投影的求解方式,能非常高效的计算Darboux型障碍函数,实验结果能证明本文提出的算法具有高效性.·提出一种新的基于BMI模型求解的障碍函数生成方法.首先利用SOS松弛方法将经典的微分障碍函数验证模型转化为一类BMI约束求解模型.本文进一步针对一般化BMI约束求解问题进行研究,最终给出求解一般BMI约束问题的变向增广拉格朗日迭代方法(Alternating Direction Augmented Lagrangian Method)的显式表达式.将该结果用于障碍函数生成问题,并给出求解算法.与当前主流软件PENNON核心算法进行比较,本文求解算法复杂度更低.·提出新的系统抽象方法.针对复杂的非线性混成系统模型本身进行研究,提出线性抽象的构造方法,避免了通过直接求解复杂的原系统障碍验证所造成的高计算复杂度.将给定的非线性混成系统转化成相应的具有待定参数的线性抽象系统,接着对抽象得到的线性系统运用量词消去方法进行线性障碍验证生成,该线性混成系统的安全性同时保证了原系统的安全性.实验证明,本文提出的基于线性抽象的障碍函数生成,能解决原本直接利用量词消去不能解决的非线性系统安全问题.
[Abstract]:Hybrid systems are a class of complex dynamical systems, which contain both continuous evolution behavior and discrete transition behavior, and both occur intertwined. The continuous evolution state can be used to describe the continuous behavior of individual physical hardware. Discrete transition states can be used to describe discrete control or switching behavior in different modes. With the rapid development of information technology and manufacturing engineering, the hybrid system can be used in the formal analysis and modeling research of embedded system and its derived information physics fusion system (CPS). Embedded systems and CPS are widely used in many safety related fields, such as aerospace, intelligent transportation, medical and health, etc. It has become a hot and frontier research topic in the field of software engineering to study the security problems of hybrid systems by combining mathematics and computer methods. It has important scientific value and practical significance. The obstacle function generation method is one of the main methods for security verification of hybrid systems. Because of avoiding the difficulty of computing the state reachability set of hybrid systems, the key problem of this kind of method lies in two aspects: on the one hand, the existing obstacle verification conditions are too conservative; on the other hand, The computational complexity of the obstacle verification condition solving model is high. In this paper, the obstacle function generation method of the hybrid system is studied in depth, from the following three aspects: create a new low constraint obstacle verification condition, Simplify the calculation of obstacle function generation model, The abstract method of complex system model further reduces the computational complexity of obstacle function generation. The main achievements and contributions of this paper are as follows: 路A new obstacle verification condition is proposed. This paper is based on the use of Darboux. A class of barrier functions constructed by special properties of polynomials, It is called Darboux type obstacle function generation. Because of the new security verification condition construction method, it can generate obstacle function that existing obstacle verification method can not generate, which can also be explained by the experimental results. In addition, Due to the special characteristics of the problem model transformed by the Darboux obstacle verification condition, this paper proposes a solution method of LS-QP cross-projection, which can calculate the Darboux type obstacle function very efficiently. The experimental results show that the proposed algorithm is efficient. 路A new method of generating obstacle function based on BMI model is proposed. Firstly, the classical differential obstacle function verification model is transformed into a new one by using SOS relaxation method. In this paper, we further study the generalized BMI constraint solving problem. Finally, the explicit expression of the variable augmented Lagrangian iterative method for solving general BMI constraint problem is given. The result is used to generate the obstacle function. Compared with the current mainstream software PENNON core algorithm, the complexity of this algorithm is lower. A new system abstraction method is proposed, and the complex nonlinear hybrid system model itself is studied. A linear abstract construction method is proposed to avoid the high computational complexity caused by the direct solution of complex original system obstacles. The given nonlinear hybrid system is transformed into the corresponding linear abstract system with undetermined parameters. Then the linear system is verified and generated by quantifier elimination method. The security of the linear mixed system is also guaranteed. The obstacle function generation based on linear abstraction proposed in this paper can solve the security problems of nonlinear systems which can not be solved by using quantifiers directly.
【学位授予单位】：华东师范大学
【学位级别】：博士
【学位授予年份】：2017
【分类号】：O19

【相似文献】