基于概率模型检验的cbc通信协议验证

基于概率模型检验的cbc通信协议验证

随着计算机网络和通信技术的发展，基于通信的运营权限（cct）已经成为人们研究的重点。cbt系统独立于轨道电路。高精度列车定位和多段式高速双向数据的数据。它通过驾驶员和基地设施实现列车控制，这是针对铁路控制系统的发展。方向,可满足铁路运输智能化、信息化和网络化的发展需要.车地间无线通信是CBTC系统的关键技术之一.而通信协议作为车地间无线通信的基础,也是CBTC系统重要的组成部分,它的正确性、稳定性和安全性对整个系统有重要影响.传统的通信协议验证方法主要是通过模拟和仿真,可是,模拟和仿真不能保证完全的错误覆盖,同时这两种方法所消耗的时间也是惊人的.形式化验证技术用数学的方法验证一个设计的功能与性能,能保证对所有的情况进行验证,在系统设计中得到了广泛的应用.因此,对通信协议进行形式化验证是很有意义的.CBTC系统车地间无线通信信道具有随机特征,因此,CBTC系统的通信子系统亦呈现明显的统计特征,这导致某些具有随机特征的变量以参数的形式引入到通信协议中.目前,针对随机特征的研究方法主要集中于随机Petri网的形式化验证.可是,由于缺乏时态逻辑的支持,随机Petri网在描述事件发生的逻辑顺序方面存在缺陷,从而限制了随机Petri网的应用.鉴于此原因,本文作者探讨用概率模型检验对CBTC系统通信协议进行形式化验证.概率模型验证是一种形式化验证方法,适用于验证具有随机特征的模型.概率模型检验采用多端点二叉判决图(MTBDDs)数据结构,很好地解决了状态空间爆炸问题.同时,概率模型检验有时态逻辑的支持,弥补了随机Petri网在描述事件发生的逻辑顺序方面存在的缺陷.本文作者的主要工作是:①综合了CBTC系统车地通信协议失效的随机错误;②设计了车地安全通信协议;③建立了通信协议的概率模型,用概率模型检验对其进行形式化验证.1关于cbt系统的一般介绍CBTC中,车地通信工作分为3个阶段:链接的建立、维持和释放.11连接建立只有发起方有权主动建立链接,跟随方接收到发起方的建链命令RFC后才能响应,见图1(a).22链接维护通信双方每个周期只进行一次数据交互.如果应用没有产生任何数据,通信协议需要生成心跳信息以维持链接,见图1(b).32连接释放只有发起方才能主动释放链接.当发起方不需要链接时,向通信协议下达释放链接命令,通信协议主动释放发起方的链接,见图1(c).2概率模型试验2.1马尔可夫判决过程、连续时间马尔可夫链模型在概率模型检验中,有3类模型:离散时间马尔可夫链(DTMCs),马尔可夫判决过程(MDPs)及连续时间马尔可夫链(CTMCs).本文不详细介绍3类模型的具体细节,因为这不是本文工作重点,3类模型的详细介绍参见文献.2.2状态公式[][]概率模型验证中,用概率计算树逻辑PCTL(ProbabilisticComputationalTreeLogic)来刻画DTMCs和MDPs,用CSL刻画CTMCs.PCTL是计算树逻辑CTL的概率性扩展,其基本语法如下:ϕ::=true|a|ϕ∧ϕ|¬ϕ|P⊳⊲p[ψ]‚ψ::=Xϕ|ϕU≤kϕ|ϕUϕ.ϕ::=true|a|ϕ∧ϕ|¬ϕ|Ρ⊳⊲p[ψ]‚ψ::=Xϕ|ϕU≤kϕ|ϕUϕ.这里,需要区分状态公式ϕ和路径公式ψ,它们分别用来评价状态和路径.a是一个原子命题,ᐅᐊ∈{≤,<,≥,>},p∈,k为正整数.时态运算符X(neXt)与U(Until)同传统的CTL定义一致.Xϕ为真,表示ϕ在当前状态的下一个状态上成立;ϕ1U≤kϕ2为真,表示存在某一状态ω(i)(i≤k),ϕ2在ω(i)上成立,而对于在ω(i)之前的所有状态,ϕ1都成立;ϕ1Uϕ2为真,表示存在某一状态ω(i)(i≥0),ϕ2在状态ω(i)上成立,而ϕ1在状态ω(i)之前的所有状态上都成立.PCTL基本语义如下,对于状态s∈S:s|true⇔对所有s∈S,s|=a⇔a∈L(s),s|=ϕ1∧ϕ2⇔s|=ϕ1∧s|=ϕ2,s|=⇁ϕ⇔s|≠ϕ,s|=Pᐅᐊ[ψ]⇔ps(ψ)ᐅᐊp,这里,ps(ψ)=Probs({ω∈Paths|ω|=ψ}).对于路径ω:ω|=Xϕ⇔ω(1)有意义,并且ω(1)|=ϕ,ω|=ϕ1U≤kϕ2⇔∃i≤k.ω(i)|=ϕ2∧ω(j)|=ϕ1∀j<i,ω|=ϕ1Uϕ2⇔∃k≥0.ω|=ϕ1U≤kϕ2.CSL的基本语法和语义与之类似,本文不作详细描述,参见参考文献.3环境状态间的信息转移CBTC系统的通信协议中有3个模块:发起方、跟随方和信道.其中,信道具有典型的随机特征.另外,通信协议数据的收发也伴有随机性的延时.根据通信协议的原理,图2中的(a)、(b)和(c)分别抽象出了通信协议3个模块的概率模型.对图2作几点说明:状态间没有标记转移概率的,默认其转移概率为1,标记转移概率的,其转移概率等于标记值.每一个转移都对应一系列原子命题及动作,带有“=”号,或关系符号“>,>=,<,<=”的,都是原子命题.一个转移中标记的所有原子命题为真,则发生相应的状态转移.带有符号“:=”的表示动作,当发生某个状态转移时,伴随着相应的动作.比如说,当“rack=FALSE&nack>=5*T”为真时,发起方由状态“WAIT-ACK”转移到状态“NEW-FRAME”,同时将nack置零.图2中弧线旁边标注的数字表示的是状态转移的条件,各数字对应的具体条件见表1.图2中各状态及变量含义分别见表2、表3.4pctal的概率规范本节用概率模型检验工具PRISM对CBTC系统通信协议进行形式化验证.我们的形式化验证运行在主频为3.00GHz,内存空间为512MB的PC机中.构建模型共耗时0.25s,累计状态集合18736个,其中包含一个初始状态,状态转移共计83379个,非确定性选择共计68038种.我们需要验证的是CBTC系统通信协议典型的概率规范,以期它能达到期望的性能指标.对于通信协议来说,最关注的莫过于失效率与稳定性.由此,总结出以下典型的概率规范,并将其转化为PCTL描述的PRISM语言.规范1:若应用软件不要求释放链接,在不同的信道和系统无故障概率下,通信协议可以保持链接维持状态的概率是多少?PRISM语言:Pmax=?[(disconnect=false)U(s=3)&(r=2)];(说明:变量含义与上节中各状态的含义一致;s=0、1、2、3、4分别表示发起方处于IDLE、NEW-FRAME、WAIT-ACK、DATA、HALT状态;r=0、1、2、3分别表示跟随方处于IDLE、RECV-RFC、DATA、HALT状态,下同)规范1的验证结果如图3(a).规范2:发起方通信中断的最大概率是多少?PRISM语言:Pmax=?[trueU(s=4)];规范2的验证结果如图3(b).规范3:跟随方通信中断的最大概率是多少?PRISM语言:Pmax=?[trueU(r=3)];规范3的验证结果如图3(c).从上述验证中可以看出,信道正常概率越大且系统无延时概率越大,协议链接维持的概率也越大.定量考虑,从图3(a)可以看出,当p1=0.99,p2=0.99时,协议链接维持概率达到0.961,已具有一定的稳定性,可以作为我们设计的参考指标.失效率方面,无论是发起方还是跟随方,通信中断的概率都小于1.5×10-10.根据CBTC系统通信协议典型概率规范的验证结果,可以认为,我们设计的通信协议有比较好的稳定性,以及低水平的失效率,具有良好的实用价值.5验证了系统的稳定性本文作者综合了CBTC系统通信协议中某些参数的随机特征,用概率模