信息物理融合系统(Cyber physical Systems,简称CPS)是软件和硬件设备紧密联系、相互影响相互作用的新一代智能系统。随着自动化、通信以及计算机技术的不断发展,CPS逐渐走向成熟并越来越多的应用到实际生产和生活中。人们对于CPS的要求已经不再局限于系统的功能扩展,CPS的性能指标开始被重视。在保证系统安全性和可靠性的前提下,人们倾向于采用性能更加优秀的系统。目前关于对CPS性能评价相关的形式化方法研究还很少,本次课题在对CPS特征和性能指标相关研究整理和总结的基础上,提出将形式化建模和分析的方法引入到CPS的性能评价中。利用统计模型检测和性能评价语言连续时间随机语言(Continuous Time Stochastic Language,简称CSTL)对基于HPCCS的CPS模型进行性能评价。本文的创新点如下:(1)本文在进程演算TCCS的基础上扩展概率选择和微分方程,提出一种新的信息物理融合系统建模语言HPCCS。体系结构分析与设计语言(Architecture Analysis and Design Language,简称AADL)是一种常用的体系化建模语言,利用AADL可以方便地对大型系统建模,如航电系统、列控系统等。通过扩展AADL随机行为和混成附件,提出用于CPS建模的混成AADL建模规范。由于AADL是半形式化建模语言无法直接对其进行形式化验证,本文提出AADL到HPCCS的模型转换算法,通过对转换后的HPCCS模型检测实现检测AADL模型的目的。(2)信息物理融合系统的性能评价需要一个表达能力足够并且不存二义性的性能评价语言,本文在PLTL和CTL的基础上提出一种性能评价语言CTSL。通过基于实值状态公式的CTSL可以刻画传统时序逻辑无法描述的系统性能指标。文中通过实例说明如何使用CTSL公式描述系统性能指标。(3)为了求解给定HPCCS模型的CTSL公式结果,首先利用离散化算法将模型离散化,然后通过对离散化模型的路径遍历计算出CTSL公式的精确解。由于精确求解算法随着并发进程数的增加面临状态空间爆炸的问题,本文采用贝叶斯统计模型检测算法,将CTSL分为四类公式,根据四类公式的性质分别给出贝叶斯性能评价算法。通过本文提出的贝叶斯性能评价算法,提高CTSL公式计算的效率。同时贝叶斯性能评价算法分析可以提供反例信息,供开发者找到系统的性能瓶颈。