随着嵌入式技术、计算机技术和网络技术的不断发展，以及硬件产品性能和数据处理能力的不断提升，物联网技术得到快速发展。在此背景之下，信息-物理融合系统（Cyber-Physical Systems, CPS）作为一种新型嵌入式网络系统应运而生，并且引起了各国政府、学术界和工业界的高度重视。CPS是融合了计算和物理进程的复杂嵌入式网络系统，它通过嵌入式系统和网络对物理设备进行监测和控制，并通过反馈机制相互影响。CPS通常广泛用于重要基础设施的监测与控制、国防武器系统、医疗保健和智能交通等诸多安全攸关领域。由于物理环境通常具有不确定性以及物理设备本身可能出现故障，如何保证CPS的可信性成为一项重大的挑战，而CPS的可信性与CPS软件的可信性密切相关，因此保证CPS软件可信十分重要。形式化验证技术是提高软件可信性的一种重要技术，模型检测技术是软件验证时经常采用的形式化技术。传统模型检测技术的应用受到系统状态空间大小的限制，而CPS的状态空间巨大。统计模型检测是基于仿真和统计评估技术验证大型复杂系统的一种模型检测技术，可以对无限状态系统进行验证。针对传统模型检测技术难以验证CPS软件的问题，本文采用统计模型检测技术，围绕CPS软件属性验证领域所涉及的三个核心步骤：CPS软件形式化建模、CPS软件属性静态验证及CPS软件属性运行时动态验证展开研究。首先，以混成自动机为基础，通过引入通信端口得到扩展混成自动机，建立一个可以有效表达CPS软件行为的形式化模型；其次，基于统计模型检测技术，提出一种能够对CPS软件的行为属性进行静态验证的方法；最后，对CPS模型进行改进，考虑到环境因素对CPS运行结果的影响，对CPS中的不确定性等进行建模，并研究了CPS软件属性的运行时动态验证方法。使用统计模型检测技术对CPS软件属性进行验证，可以有效避免传统模型检测技术必须面对的状态空间爆炸问题，提升了CPS的健壮性和安全性。