文档介绍：硕士学位论文

论文题目基于时空 Petri 网的 CPS 建模与验证研究
研究生姓名张茗泰
指导教师姓名张广泉
专业名称计算机软件与理论
研究方向物联网软件工程
论文提交日期 2013 年 4 月
基于时空 Petri 网的 CPS 建模与验证研究中文摘要
基于时空 Petri 网的 CPS 建模与验证研究
中文摘要
信息物理融合系统(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 应用的普及。

关键字:信息物理融合系统;空间信息;物理实体;时空 Petri 网
作者:张茗泰
指导老师:张广泉

I
Abstract Research on Modeling and Verification of CPS based on spatial-temporal
Research on Modeling and Verification of CPS based on
Spatial-Temporal
Abstract
CPS is plex system fused puting system, physical
environment work environment. Through 3C operation, integration and depth of
collaboration, CPS control precisely physical entities to in the physical environment,
achieving real-time sensing and dynamic control of the physical environment. CPS is an
integration puting, communication and control, which is more reliable, efficient
than traditional embedded systems, and has a stronger puting
processing power. CPS has a wide range of application prospects, which is the
development direction of future embedded systems.
However, CPS not only has the advantages above, but also faces enormous
challenges. Since CPS is a kind of large, heterog