一种面向CPS的自适应统计模型检测方法

随着计算机与物理环境的交互日益密切,信息物理融合系统（cyber physical systems,CPSs）在健康医疗、航空电子、智能建筑等领域有着广泛的应用前景,CPSs的正确性、可靠性分析已引起人们的广泛关注.统计模型检测（statistical model checking,SMC）技术能够对CPSs进行有效验证,并为系统的性能提供定量评估.然而,随着系统规模的日益扩大,如何提高统计模型检测技术验证CPSs的效率,是目前所面临的主要困难之一.针对此问题,本文首先对现有SMC技术进行实验分析,总结各种SMC技术的受限适用范围和性能缺陷,并针对贝叶斯区间估计算法（Bayesian Interval Estimate,BIE）在实际概率接近0.5时需要大量路径才能完成验证的缺陷,提出一种基于抽象和学习的统计模型检测方法AL-SMC.该方法采用了主成分分析、前缀树约减等技术,对仿真路径进行学习和抽象,以减少样本空间.接着,提出了一个面向CPS的自适应SMC算法框架,可根据不同的概率区间自动选择AL-SMC算法或者BIE算法,有效应对不同情况下的验证问题.最后,结合经典案例进行实验分析,实验结果表明自适应SMC算法框架能够在一定误差范围内有效提高CPSs统计模型检测的效率,为CPSs的分析验证提供了一种有效的途径.