安全性问题贯穿信息物理融合系统建模、分析、设计、开发与维护整个系统生命周期。信息物理融合系统中的安全性问题内涵丰富、形式多样、广泛存在。本文基于动力系统的视角,以混成系统建模信息物理融合系统动力学过程,形式化的界定信息物理融合系统安全性问题为相应混成系统状态轨线与系统规约不安全点集相交性判定。信息物理融合系统生命周期涵盖多个阶段,每个阶段存在不同场景。这种状况造成信息物理融合系统安全性问题虽内涵统一,但具体存在形式却千差万别。把握决定系统安全性的主要因素,合理抽象安全性验证情景是信息物理融合系统安全性验证研究的前提和基础。总体来说,系统行为机制、控制机制和结构机制是影响系统安全性状况的关键因素。有鉴于此,信息物理融合系统安全性验证可以抽象为针对混成系统特定行为机制、控制机制与结构机制安全性的判定。基于这样的认识,本文以信息物理融合系统为背景,面向系统安全性验证问题,致力于发展以混成系统行为机制、控制机制与结构机制等的安全性为核心的形式化验证理论与方法。系统状态的连续演化、脉冲跳变与模式切换是混成系统行为的基本形式,三者在状态空间划分约束下的交互构成了混成系统行为机制的内容。针对混成系统行为机制安全性,本文介绍了以栅栏函数(barrier certificates)定理为核心的安全性判定理论和以栅栏函数构造定理为核心的判定方法。闭环的反馈控制与开环的驻留时间控制是混成系统控制的基本形式,状态反馈控制与驻留时间约束是混成系统控制机制的主要内容。本文选取模式相关驻留时间切换策略与区间驻留时间切换策略为控制机制安全性验证研究的对象,分别给出相应的栅栏函数定理及其构造定理,发展针对这两种驻留时间驱动控制机制安全性验证的理论与方法。切换型混成系统的串级与脉冲型混成系统的串级是串级混成系统结构的两种基本形式。本文针对串级切换型混成系统与串级脉冲型混成系统安全性的判定问题,分别给出相应栅栏函数定理及其构造定理,为系统结构机制安全性验证提供了从判定原理到判定方法的完整解决方案。全文研究工作以模式相关驻留时间切换策略、区间驻留时间切换策略、串级切换型混成系统与串级脉冲型混成系统安全性验证的解决为核心,从下四个方面完善信息物理融合系统安全性验证的研究：首先,针对混成系统行为机制安全性验证问题,本文以混成动力系统模型为基础,形式化的定义了混成系统行为,通过栅栏函数定理,论证栅栏函数存在则混成系统安全这一命题。进一步地,就栅栏函数的构造,介绍了栅栏函数构造定理及相关理论、方法和工具。其次,针对混成系统控制机制安全性验证问题,本文以驻留时间控制机制为研究对象,形式化的讨论模式相关驻留时间切换策略与区间驻留时间切换策略安全性的判定条件,给出相应栅栏函数定理。结合驻留时间约束控制机制栅栏函数的特点,给定相应栅栏函数构造定理,降低栅栏函数构造中的计算困难性。再次,针对混成系统结构机制安全性验证问题,本文以串级结构机制为研究对象,形式化的讨论串级切换型混成系统与串级脉冲型混成系统安全性判定条件,结合各自系统结构特点,通过引入类耗散不等式与小增益条件等约束,构造确保系统安全的充分条件,给出相应栅栏函数定理。进一步地,给出相应栅栏函数构造定理,促进系统结构机制安全性验证问题的自动化解决。最后,针对一种基于向量Lyapunov函数方法设计的顾前顾后型车辆跟随反馈控制律的“防碰撞”安全需求的验证问题,给出基于栅栏函数的验证方法。