Self-Adaptive Statistical Model Checking Approach for CPS

Cyber-Physical systems (CPSs) are advanced embedded systems engaging more interaction between computer and physical environment. CPSs are widely used in the field of healthcare equipment, avionics, and smart building. Meanwhile, the correctness and reliability analysis 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 to improve the performance of SMC with the expansion of systems. To address this issue, this study explores several SMC algorithms and concludes 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 this difficulty, an algorithm, AL-SMC is proposed based on abstraction and learning techniques to reduce the size of sampling space. AL-SMC adopts some sophisticated techniques such as property-based projection, extraction and construction of prefix frequency tree. In addition, to improve the efficiency of SMC further, a framework of self-adaptive SMC algorithm, which uses the proper algorithm by probability prediction adaptively, is presented. Finally, the self-adaptive SMC approach is implemented with three benchmarks. The experimental results show that the proposed approach can improve the performance within an acceptable error range.