信息物理融合系统(Cyber Physical System, CPS)是一种融合计算系统、物理环境、网络环境的多维复杂系统。CPS通过3C操作的有机融合与深度协作，精确控制物理环境中的物理实体协同工作，实现物理环境的实时感知和动态控制。CPS实现了计算、通信与控制的一体化，与传统嵌入式系统相比更加可靠、高效，并且提升协同计算处理能力，具有广泛的应用前景，是未来嵌入式系统的发展方向。然而，CPS在具备以上优点的同时，也面临巨大难题。由于CPS是多个异构子系统通过网络相融合的大型、异构、分布式实时反馈系统，系统复杂度远超一般信息系统，同时CPS又引入了改变物理环境的控制系统，这些都给开发带来巨大困难。寻找一种适用于CPS的开发方法是目前国内外关于CPS的重要研究方向之一。时间Petri网作为分布式、并行以及实时系统建模与分析的一种重要形式化工具，为CPS建模提供了坚实基础。然而时间Petri网缺乏空间信息描述能力，因此无法完全对于CPS进行建模。本文的主要目标便是针对这个缺陷拓展时间Petri网，构造能够描述CPS物理实体位置变迁的时空Petri网。本文首先对CPS的物理层面特点进行详细分析，从物理实体的分类与特征两方面着手，深入研究CPS物理实体的属性及其位置变迁过程，提出一种CPS物理实体的形式化建模方法；其次，通过分析时空Petri网必须满足的特性，在时间Petri网基础上引入空间因素，得到时空Petri网的形式化定义，使其不仅能够描述物理实体逻辑及时间层次的行为，而且能够描述物理实体位置变迁所引起的状态变化。最后，以模型检测技术为核心思想，提出一种能够对时空Petri网模型的行为属性、时间属性以及数据属性等进行形式化验证的理论方法。对CPS物理实体建模与验证方法的深入研究可以有效提高CPS的可信性，推动CPS应用的普及。