由于嵌入式、计算机等技术的快速发展和硬件产品的性能以及在数据处理方面能力的不断提升,一些技术得到突飞猛进的发展,如物联网技术。在此背景下,信息物理融合系统(Cyber Physical Systems,CPS)进入人们的视野,并得到各国政府以及各界人士的重视,便成为一种新型嵌入式网络系统。CPS是将物理、生物及工程学巧妙融合在一起的具有局部操控性和全局控制特征的综合性系统,这种新兴的网络系统引起了研究界极大的兴趣,也是未来通信网络的一种重要发展方向。CPS通常被应用在一些对安全性要求较高的领域,如基础设施的监测与控制、国防和武器系统、医疗和智能交通等方面。CPS之所以能得到学术界的青睐,一方面就是它在建模方面的应用。CPS系统建模时不仅应该考虑时间信息,还应该考虑空间信息,而传统的嵌入式方法大多只关注这些信息当中的其中一个方面,这样显然不能满足CPS系统中复杂的通信要求。因此,我们需要考虑如何描述信息物理融合系统中的时间和空间信息并对其进行建模。虽然自动机在系统建模方面能够有效地对CPS系统的离散和连续行为进行建模,但是不能有效的对与位置相关的信息表达,尤其是对空间约束进行描述。这样,学者们便考虑在空间变量以及空间表达式方面对已有的混成系统进行扩充以提高其建模的能力,从而使得对系统的建模能够得到满足。本文致力于不确定性CPS建模与属性验证的研究,将环境的不确定性考虑进去,进而考虑环境的不确定性在CPS软件运行与动态验证方面的影响。在深入研究可能性测度与时空逻辑基础上,提出可能性时空混成自动机模型,以此给出可能性时空CPS软件体系结构模型,并对CPS体系架构建模。针对不确定性环境对CPS控制动态行为的影响,给出一种形式化的CPS软件模型描述语言——可能性时空LTL(PoStLTL),并给出验证系统属性的可能性时空响应性和可能性时空?-正则安全性。通过理论证明和实例分析CPS控制系统建模与属性验证方法在不确定环境下的可行性。