在当今高度相互关联的世界中,信息物理融合系统(Cyber-Physical Systems,CPS)将计算机系统与物理设备相连接。计算机系统与物理环境进行交互,提供了人们日常所需的各种服务,包括交通运输、建筑设备自动化、电力、水利、工业生产和医疗等。随着CPS的研究与发展,关于CPS的安全性和可靠性问题逐渐呈现。形式化方法运用数学语言对软硬件系统进行模型的抽象,能够将系统及其验证属性规范的表达出来,极大地提高了系统的可靠性和安全性,并且保证了系统安全正确的运行。由于CPS往往对时间有较高要求,并且时间自动机中包含时钟约束,本文采用时间自动机作为建模语言对CPS进行建模。本文首先对CPS的相关知识进行研究和分析,然后对系统各组件进行建模,并对建模后的模型进行安全属性验证。以水位控制系统为CPS实例,系统模型的构建包括常用组件建模、攻击者建模以及自动恢复机制建模。安全属性验证包括基于死锁算法、可达性算法和线性时序逻辑算法的验证,来对系统模型进行死锁性、时序性和安全性检测。另外,本文提出了基于属性模式的时间自动机的语言包含验证方法,对系统模型进行验证。该方法是对原有方法的改进,验证属性建模时只关注与验证相关的事件。本文的主要成果如下:(1)给出了如何使用时间自动机对CPS进行建模。以水位控制系统为例,首先将系统各个组件分别构建为一个或多个时间自动机模型,然后完成攻击者和自动恢复机制的建模,最后将各个模型组成完整系统;(2)提出了基于属性模式的时间自动机语言包含验证方法。总结并给出了几种常用属性模式的时间自动机模型,在此基础上改进了已有的时间自动机语言包含验证方法,改进后的算法能够在对验证属性建模时忽略与验证无关的事件,从而极大地简化了验证属性的建模;(3)在上述模型和验证方法的基础上,完成了对系统是否满足安全属性的验证及分析。首先对安全属性进行形式化描述,再编写对应的断言语句,最后对系统进行基于死锁算法、可达性算法、线性时序逻辑算法以及基于属性模式的语言包含验证方法的属性验证和分析。