一种面向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的分析验证提供了一种有效的途径.

Self-Adaptive Statistical Model Checking Approach for CPS

Cyber Physical Systems (CPSs) are advanced embedded systems concerning more interaction between computer and physical environment.CPSs are widely used in the field of healthcare equipment, avionics, smart building, etc.Meanwhile, the correctness and reliability analyzing of CPSs has attracted more and more attentions.Statistical model checking (SMC) is an effective technology for verifying CPSs, which facilitates the quantitative evaluation for system performance.However, it is still a challenge how to improve the performance of SMC with the expansion of systems.To address this issue, we explored several SMC algorithms and found that Bayesian Interval Estimate is the most practical and efficient algorithm.However, large scale of traces are needed when the actual probability is around 0.5 during the evaluation.To overcome the difficulty, we propose the AL-SMC algorithm based on abstraction and learning techniques to reduce the size of sampling traces.AL-SMC adopts some sophisticated techniques, i.e.property-based projection, extraction and construction of the prefix frequency tree.Besides, to improve the efficiency of SMC further, we also present a framework of self-adaptive SMC algorithm, which uses the proper algorithm by probability prediction adaptively.Finally, we implement the self-adaptive SMC approach with three benchmarks.The experimental results show that our approach can improve the performance