An Incremental Runtime Stochastic Model Checking Framework for Verifying Communication Protocols of Industrial CPS

Communication Protocol is an important part of industrial CPS, which plays a very crucial role for CPS to complete its task. Runtime stochastic model checking is widely used to verify the qualitative and quantitative properties of Communication Protocols with random behaviors. An important challenge in the verification process is that it takes too much time. It should be fast enough to respond to runtime requirements when the industrial CPS changes dynamically. In this paper, we propose an incremental runtime stochastic model checking (IRSMC) framework for verifying communication protocols of industrial CPS, based on the heuristic. IRSMC framework combines the heuristic method to decrease the verification time. It lessens the number of numerical iterations in runtime stochastic model checking, which reuses the calculated value of reachability probabilities and reorders the model states when the industrial CPS changes. We implement IRSMC framework with model checking tool PRISM, and apply it to verify communication protocol Crowds, BRP, EGL. The experiments results show that IRSMC can reduce the verification time obviously, compared with standard runtime stochastic model checking.