信息物理融合系统(Cyber-Physical Systems,CPS)是一类融合了信息处理过程与真实物理环境进程于一体的分布式实时反馈系统,包含计算、通信与控制三大功能。它不仅可以对物理环境进行实时感知,还能够通过计算与通信实现对物理实体的动态控制。CPS拥有传统系统难以企及的优势,是工业4.0中实现智能制造的核心与关键之一。CPS系统复杂,功能强大,这为它带来优势的同时也为其研究带来了困难与挑战。组成CPS的子系统在结构、功能及开发语言方面都有所不同,且它们之间存在大量的交互与协作,再加上需要对物理实体进行实时控制,增加了其复杂程度。因此,需要采用适当的建模方法,对CPS的性质与功能进行合理的描述,并进行有效的验证。Petri网拥有直观地表达系统结构以及描述异步并发事件的能力。而时间Petri网在此基础上增加了时间因素,可用于对分布式的实时系统进行建模,但对空间因素难以进行有效的表达。本文针对经典时间Petri网的不足,向其添加对空间信息的描述,使其具备描述物理实体位置变迁的能力,构造一种扩展的时间Petri网模型——时空Petri网STPN,并研究其对CPS进行建模的方法等。本文从CPS中的物理实体的属性与特征入手,对CPS的各物理模块进行分类,并给出形式化定义,对物理实体建立模型;然后通过分析CPS的性质与要求,加入空间因素,扩展经典的时间Petri网,使构造的STPN不仅可以描述系统时间层面的性能,也具备描述物理实体在空间层面上的变迁的能力,满足CPS的建模需求,并以一个带有智能机器人的信息物理生产系统(CPPS)为研究对象,建立相应STPN模型,分析了模型的可行性。最后对模型验证工具UPPAAL进行介绍与研究,描述其BNF语法与模型验证方式,以异常情况自主处理的部分为例,通过UML时序图将本文构造的STPN模型转换为UPPAAL使用的时间自动机模型,并通过CTL公式对模型的关键性质进行描述与验证,说明模型的可靠性与有效性。