基本信息来源于合作网站,原文需代理用户跳转至来源网站获取       
摘要:
通信协议是CBTC系统重要的组成部分,它的正确性、稳定性和安全性对整个CBTC系统有重要影响.鉴于通信协议中某些参数具有随机特征,本文采用概率模型检验对其进行形式化验证.分析了概率模型检验的语义及语法,建立了通信协议的概率模型,用概率模型检验工具PRISM验证了典型的概率规范.结果证明,当信道正常概率为99%,系统无延时概率为99%时,通信协议失效率小于1.5×1010.说明了用概率模型检验验证具有随机特征参数的通信协议,方法简单快捷,结论清晰明了.
推荐文章
匿名通信协议MACP概率模型检验
匿名通信
P2P
MACP
概率模型检验
基于Rebeca模型的硬件设计形式化验证
形式化验证
Rebeca模型
Modere
基于TLA的事件图模型形式化验证方法
仿真模型
验证、确认和认定
模型检验
行为时态逻辑
事件图
SIP协议系统模型的形式化研究
形式化规范
SIP协议
SDL
MSC
内容分析
关键词云
关键词热度
相关文献总数  
(/次)
(/年)
文献信息
篇名 概率模型检验的CBTC系统通信协议的形式化验证
来源期刊 北京交通大学学报 学科 交通运输
关键词 CBTC系统 通信协议 概率模型检验 形式化验证
年,卷(期) 2009,(5) 所属期刊栏目 电子信息通信工程
研究方向 页码范围 35-39
页数 5页 分类号 U238.2|TP301
字数 3147字 语种 中文
DOI
五维指标
传播情况
(/次)
(/年)
引文网络
引文网络
二级参考文献  (0)
共引文献  (0)
参考文献  (0)
节点文献
引证文献  (0)
同被引文献  (0)
二级引证文献  (0)
2009(0)
  • 参考文献(0)
  • 二级参考文献(0)
  • 引证文献(0)
  • 二级引证文献(0)
研究主题发展历程
节点文献
CBTC系统
通信协议
概率模型检验
形式化验证
研究起点
研究来源
研究分支
研究去脉
引文网络交叉学科
相关学者/机构
期刊影响力
北京交通大学学报
双月刊
1673-0291
11-5258/U
大16开
北京西直门外上园村3号
1975
chi
出版文献量(篇)
3626
总下载数(次)
7
论文1v1指导