信息物理融合系统安全性验证研究

发布时间：2018-01-12 01:26

本文关键词：信息物理融合系统安全性验证研究　出处：《华东师范大学》2016年博士论文　论文类型：学位论文

【摘要】：安全性问题贯穿信息物理融合系统建模、分析、设计、开发与维护整个系统生命周期。信息物理融合系统中的安全性问题内涵丰富、形式多样、广泛存在。本文基于动力系统的视角,以混成系统建模信息物理融合系统动力学过程,形式化的界定信息物理融合系统安全性问题为相应混成系统状态轨线与系统规约不安全点集相交性判定。信息物理融合系统生命周期涵盖多个阶段,每个阶段存在不同场景。这种状况造成信息物理融合系统安全性问题虽内涵统一,但具体存在形式却千差万别。把握决定系统安全性的主要因素,合理抽象安全性验证情景是信息物理融合系统安全性验证研究的前提和基础。总体来说,系统行为机制、控制机制和结构机制是影响系统安全性状况的关键因素。有鉴于此,信息物理融合系统安全性验证可以抽象为针对混成系统特定行为机制、控制机制与结构机制安全性的判定。基于这样的认识,本文以信息物理融合系统为背景,面向系统安全性验证问题,致力于发展以混成系统行为机制、控制机制与结构机制等的安全性为核心的形式化验证理论与方法。系统状态的连续演化、脉冲跳变与模式切换是混成系统行为的基本形式,三者在状态空间划分约束下的交互构成了混成系统行为机制的内容。针对混成系统行为机制安全性,本文介绍了以栅栏函数(barrier certificates)定理为核心的安全性判定理论和以栅栏函数构造定理为核心的判定方法。闭环的反馈控制与开环的驻留时间控制是混成系统控制的基本形式,状态反馈控制与驻留时间约束是混成系统控制机制的主要内容。本文选取模式相关驻留时间切换策略与区间驻留时间切换策略为控制机制安全性验证研究的对象,分别给出相应的栅栏函数定理及其构造定理,发展针对这两种驻留时间驱动控制机制安全性验证的理论与方法。切换型混成系统的串级与脉冲型混成系统的串级是串级混成系统结构的两种基本形式。本文针对串级切换型混成系统与串级脉冲型混成系统安全性的判定问题,分别给出相应栅栏函数定理及其构造定理,为系统结构机制安全性验证提供了从判定原理到判定方法的完整解决方案。全文研究工作以模式相关驻留时间切换策略、区间驻留时间切换策略、串级切换型混成系统与串级脉冲型混成系统安全性验证的解决为核心,从下四个方面完善信息物理融合系统安全性验证的研究：首先,针对混成系统行为机制安全性验证问题,本文以混成动力系统模型为基础,形式化的定义了混成系统行为,通过栅栏函数定理,论证栅栏函数存在则混成系统安全这一命题。进一步地,就栅栏函数的构造,介绍了栅栏函数构造定理及相关理论、方法和工具。其次,针对混成系统控制机制安全性验证问题,本文以驻留时间控制机制为研究对象,形式化的讨论模式相关驻留时间切换策略与区间驻留时间切换策略安全性的判定条件,给出相应栅栏函数定理。结合驻留时间约束控制机制栅栏函数的特点,给定相应栅栏函数构造定理,降低栅栏函数构造中的计算困难性。再次,针对混成系统结构机制安全性验证问题,本文以串级结构机制为研究对象,形式化的讨论串级切换型混成系统与串级脉冲型混成系统安全性判定条件,结合各自系统结构特点,通过引入类耗散不等式与小增益条件等约束,构造确保系统安全的充分条件,给出相应栅栏函数定理。进一步地,给出相应栅栏函数构造定理,促进系统结构机制安全性验证问题的自动化解决。最后,针对一种基于向量Lyapunov函数方法设计的顾前顾后型车辆跟随反馈控制律的“防碰撞”安全需求的验证问题,给出基于栅栏函数的验证方法。
[Abstract]:Safety problems through the physical information fusion system modeling, analysis, design, development and maintenance of the whole system life cycle. The connotation of physical information fusion system security in the rich, diverse forms, widely exist. This paper based on the perspective of power system, the hybrid system modeling physical information fusion system dynamic process, the formal definition of information physical system security problem to determine the corresponding intersection of the trajectory of hybrid system and system security statute does not set. Physical information fusion system life cycle covers multiple stages, each stage in different scenes. This situation caused by the physical information fusion system security problem is the connotation of unity, but the forms are different. To grasp the decision the main factors of system safety, reasonable abstract security verification scenario is the study of system security verification before physical information fusion And provided basis. In general, the behavior of the system mechanism, control mechanism and structure mechanism is a key factor affecting the system security situation. In view of this, the physical information fusion system security verification can be abstracted as the specific behavior of hybrid system, decision control mechanism and structure of system security. Based on this understanding, this paper based on information physical system as the background, system oriented security verification, committed to the development of the hybrid system behavior mechanism, security mechanism and control mechanism of the structure is the core of the formal verification theory and method. The continuous evolution of the system state, pulse and mode switching is the basic form of hybrid system behavior, interaction three in the state space partition constraints constitute a hybrid system behavior mechanism of the content. For the hybrid system security mechanism, this paper introduces the barrier function (bar Rier certificates) safety decision theorem as the core of the theories and methods on barrier function structure theorem as the core. The closed-loop feedback control and open-loop control of dwell time is the basic form of hybrid system control, state feedback control and dwell time constraints is the main content of hybrid system control mechanism. This paper selects patterns related to reside time switching strategy and interval dwell time switching strategy to control the mechanism to verify the safety of the object of study, were given the barrier function theorem and its structure theorem, the development of the two kinds of dwell time drive theory and method of control mechanism for security verification. Cascade switched hybrid system with cascade pulse type hybrid system is on the two basic forms of hybrid system level structure. In this paper the cascade switched hybrid system with cascade safety type hybrid system pulse judgment Fixed problem are given the corresponding barrier function theorem and its structure theorem, provides a solution to the principle from the judging method to determine the complete solution for system security verification. The mechanism and structure of the research work related to mode of dwell time switching strategy, interval dwell time switching strategy, cascade switched hybrid systems and solve the security level pulse string hybrid system verification is the core of information fusion system, physical security verification perfect from the following four aspects: first, the hybrid system behavior and mechanism of the safety verification problem, based on the hybrid power system model, the formalization of hybrid system behavior, through the fence function theorem, proof fence function is this hybrid system security proposition. Further, the structural barrier function, the barrier function construction theorem and the related theories, methods and tools. Time for hybrid system verification of safety control mechanism, based on the dwell time control mechanism as the research object, formal discussion mode related dwell time switching strategy and interval dwell time switching strategy safety conditions, the corresponding barrier function theorem. Combining the dwell time constraint control mechanism of barrier function, given the corresponding structure the fence function theorem, reduce the difficulty of computing the barrier function structure. Thirdly, according to the structure of hybrid system security mechanism based on the verification problem, cascade structure mechanism as the research object, discuss the form of cascade switched hybrid system with cascade pulse type hybrid system safety conditions, combined with their structural characteristics of the system, by introducing dissipative inequality and small gain conditions and other constraints, sufficient conditions to ensure the security of the system structure, the corresponding fence function theorem. Further, the corresponding structural barrier function theorem, promote automation system structure security verification mechanism to solve the problem. Finally, according to the design of a vector Lyapunov function method of front and back information vehicle following feedback control law based on the "collision" safety requirements verification problem, given verification method based on the function of the fence.

【学位授予单位】：华东师范大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：TP309

【相似文献】