Framework For Predict CPS Rare Event Based On Statistical Model Checking

With the wide application of Cyber-Physical System and its related technologies in real life,the security of CPS has attracted more and more public attentio.The rich application scenarios of CPS lead to the growth of system's uncertainty.The uncertainty of CPS indicates that the security of CPS is not only related to the specifications of system design,but also needs to take the influence of rare events on the security of CPS into consideration.Since the application of CPS in security-related fields like aerospace,weapons,medical equipment and so on.Once the security issues occur,it will threaten people's lives and properties.It is important to verify the CPS security issues caused by uncertain rare events.This thesis proposes a CPS rare event state sequence sampling techniques based on statistical model checking for capturing CPS rare event training sample set.With the sample set,this paper designs a CPS rare event prediction method based on Hidden Markov Model to predict the probability of rare events in CPS.Using the CPS rare event state sequence sampling techniques and CPS rare event prediction method,this thesis designs a framework for predict CPS rare event based on statistical model checking.This framework takes system hybrid automata model and system property specification as input,and realizes real-time simulation in Simulink by model transformation.In the real-time running of the system,On the one hand,the CPS rare event state sequence sampling method constucts the optimal sampling distribution,then we get the relationship between the maximum expectation of the rare event state sequence and the initial state,to improve the sampling efficiency.On the other hand,the rare event prediction method based on Hidden Markov Model uses the sampled rare event states sequence to train the model.Then we evaluate the Hidden Markov Model's efficiency by AUC(Area Under Curve).The Hidden Markov Model can output the probability that the sequence will evolve into a rare event state sequence.This thesis verifies the feasibility of CPS rare event prediction framework based on statistical model test through experiments.We also illustrate the advantages of related technologies used in this framework through comparative experiments.Furthermore,we prove that the framework can make effective contributions in solving practical CPS problems.