信息物理融合系统是近年来研究的一个热点领域,它集成了计算成分和物理成分,这类系统具备计算、通信及控制行为能力,包含离散和连续混合特性,往往应用于安全攸关的领域,如智能交通、航天航空、医疗保健等领域,对系统运行的安全特性等具有很高要求。因此,建立一个安全可靠的信息物理融合系统模型成了一项具有重要理论意义和应用价值的课题。　　一般情况下,应用于系统的多级安全模型主要可分为两类,即访问控制安全模型和信息流安全模型。访问控制安全模型主要通过限制访问主体对访问客体的访问权限,使得系统信息流在合法范围内流动;访问控制安全模型的策略和机制决定用户能做什么和不能做什么,因此它侧重于强调如何才能保证系统的信息流安全,它不能有效解决隐通道信息泄露问题。信息流安全模型主要研究系统信息流事件运行轨迹之间的特定等价关系,因此它侧重于强调安全是什么,它能有效解决隐通道信息泄露问题。因此,就刻画信息物理融合系统安全本质而言,信息流安全模型更为适合。　　然而信息流安全模型基于不同的语义,相互间很难进行比较和分析。本文主要采用安全进程代数和Petri网两种形式化方法对信息物理融合系统的信息流安全模型从代数层次和结构层次上进行分析,主要目的为方便信息流安全模型间的相互比较的同时也能体现信息流安全特性分析方法多样性。　　本文在对比分析多级安全模型和形式化定义信息流安全模型的基础上,给出了信息流安全模型的验证算法和验证工具;利用着色Petri网对天然气管道信息物理融合系统进行了建模,并利用CPN-Tools得到的状态图对天然气管道网络信息流安全进行了分析:利用安全进程代数对天然气管道网络系统的信息流事件进行了建模和分析;基于迹语义分析了天然气管道网络系统的非演绎和非确定性非干扰两种信息流安全模型;分别利用安全进程代数和Petri网从语言层次和结构层次对天然气管道系统组合后的非演绎和非确定性非干扰信息流安全模型的保持问题做了深入研究,并给出了相关结论。　　本文的主要创新工作:　　(1)提出了基于安全进程代数对比研究多级安全模型的方法,研究了六种主要的信息流安全模型的逻辑蕴含关系。给出了基于迹语义的六种信息流安全模型的验证算法,并且开发了相应的验证工具。　　由于分级安全模型大多基于不同的语义模型,导致了相互间难以进行比较和分析。另外通用的信息流安全模型的验证工具比较少,因此本文的第一个工作主要是基于安全进程代数对各种信息流安全模型进行了比较研究,给出了各自的验证算法及工具。　　(2)给出了基于着色Petri网的信息物理融合系统模型,并利用CPN Tools得到的状态图对信息物理融合系统的安全做了简要分析。基于安全进程代数提出了对信息物理融合系统的信息流事件的建模方泫。　　由于信息物理融合系统中大量存在计算成分、物理设备及两者之间的相互依赖关系,给系统及信息流安全模型的建模和分析带来了难度,因此本文的第二个工作是研究了信息物理融合系统及其信息流事件的建模方法。　　(3)提出了基于Petri网的信息物理融合系统非演绎模型及其组合的分析和构造方法。基于Petri网定义了了四种组合方式,给出了按这四种方式组合后的信息物理融合系统仍能满足非演绎特性的充分必要条件,并给出了证明方法。　　任何系统都不是独立存在的,必然和这样那样的系统存在交互和联系;另外,“分治法”在设计大规模的信息物理融合系统时是一种很有效的方法,因此研究系统的组合问题特别重要。　　(4)提出了基于安全进程代数的信息物理融合系统的非确定性非干扰模型及其组合的分析和构造方法。系统组合的方式虽然有很多种,但从有无反馈环的角度来说只有瀑布组合和反馈环组合方式两种方式。在定义瀑布组合和反馈环组合的基础上,给出了按这两种方式组合后的信息物理融合系统仍能满足非确定性非干扰特性的充分必要条件,并给出了证明方法。