概率模型检验的CBTC系统通信协议的形式化验证

通信协议是CBTC系统重要的组成部分，它的正确性、稳定性和安全性对整个CBTC系统有重要影响．鉴于通信协议中某些参数具有随机特征，本文采用概率模型检验对其进行形式化验证．分析了概率模型检验的语义及语法，建立了通信协议的概率模型，用概率模型检验工具PRISM验证了典型的概率规范．结果证明，当信道正常概率为99％，系统无延时概率为99％时，通信协议失效率小于1．5×10^-10．说明了用概率模型检验验证具有随机特征参数的通信协议，方法简单快捷，结论清晰明了．

Formal Verification for Communication Protocol of CBTC System Based on Probabilistic Model Checking

Communication protocol is one of the most important components in the CBTC system, the correctness and stableness and security of the communication protocol are very important to the whole CBTC system. For some parameters of the communication protocol representing stochastic character, this paper makes a formal verification by probabilistic model checking. The paper analyses the semantics and syntax of the probabilistic model checking, and constructs a probabilistic model for the communication protocol, and uses a probabilistic model checking tool PRISMto implement a formal verification. The result proves that, when the probability of channel being natural is 99%, and the probability of the system without delaying is 99%, the failure probability of the communication protocol less than 1.5×10^-10. It is also proves that, by using probabilistic model checking to verify the communication protocol which with some stochastic parameters, not only the method is simple and rapid, but also the conclusion is clear.