信息物理融合系统(Cyber Physical System,CPS)是一个集计算系统、通信系统、感知系统、控制系统和物理系统为一体的复杂系统。通过对物理环境和资源的动态感知、信息的实时可靠传输、数据的综合计算处理,并利用反馈循环实现对物理过程的有效控制。整个CPS的运行过程既包含自然世界连续的物理进程,又包含信息世界离散的计算进程,是一种二者深度融合并紧密交互的混成行为。Petri网作为一种用令牌流动的方式来表示系统动态变化的网络,适合于描述具有并发、异步、不确定性等特征的系统。传统的Petri网是一种离散模型,无法描述系统连续变量的演化。混成Petri网是建模混成系统的有力工具之一,本文在此基础上进行改进提出扩展混成Petri网模型。随着CPS在航空航天、工业控制、医疗设备等安全关键领域的应用越来越广泛,人们对系统的安全性与可靠性需求也逐渐增加,因此,如何保障系统可靠性是人们关注的一大问题。本文围绕CPS的建模与分析展开,具体工作如下:(1)针对CPS的离散与连续融合特性,以混成Petri网为基础模型,考虑到某些系统的时间属性,在基础模型上添加时间约束并引入抑止弧和测试弧的概念,由此构建扩展混成Petri网模型。(2)针对CPS应用中无人驾驶车辆系统的两个不同的场景,采用扩展混成Petri网模型具体阐述如何使用该模型对CPS系统进行建模并分别通过仿真与验证的方法进行分析。关于仿真,首先将建立的模型按照一定的规则转化为与之对应的Simulink模型,并通过Matlab对系统行为及属性进行分析。关于验证,本文首先针对扩展混成Petri网模型提出状态演化图的构造算法,并针对演化图,运用有界模型检测的思想,将模型检测问题转化为可满足性问题。最后通过SMT工具Z3进行求解分析。