基本信息来源于合作网站,原文需代理用户跳转至来源网站获取       
摘要:
计算机联锁系统是铁路信号控制系统的核心设备,是有着苛刻安全要求的复杂控制系统.本文采用Prover形式化开发工具对联锁软件安全需求进行形式化验证.通过模型检验的形式化验证方法,遍历系统输入变量的所有状态空间,验证联锁特定应用满足系统安全需求,确保系统的安全性得以正确实现.在保证系统安全性的基础上,以全状态空间查找反例的检验方法进一步提升产品的质量.
推荐文章
基于Rebeca模型的硬件设计形式化验证
形式化验证
Rebeca模型
Modere
基于活性顺序图的形式化验证方法及工具研究
活性顺序图
形式化验证
软件开发过程
基于TLA的事件图模型形式化验证方法
仿真模型
验证、确认和认定
模型检验
行为时态逻辑
事件图
应用ETDFA生成CBTC联锁软件形式化模型的方法
CBTC
联锁软件
ETDFA
形式化方法
内容分析
关键词云
关键词热度
相关文献总数  
(/次)
(/年)
文献信息
篇名 基于Prover的联锁软件形式化验证过程研究
来源期刊 铁道通信信号 学科
关键词 联锁软件 形式化验证 模型检验 安全需求
年,卷(期) 2020,(3) 所属期刊栏目 信号·控制
研究方向 页码范围 17-21
页数 5页 分类号
字数 3632字 语种 中文
DOI 10.13879/j.issn1000-7458.2020-03.19434
五维指标
作者信息
序号 姓名 单位 发文数 被引次数 H指数 G指数
1 张程 2 1 1.0 1.0
2 王燕芩 4 5 2.0 2.0
传播情况
(/次)
(/年)
引文网络
引文网络
二级参考文献  (28)
共引文献  (16)
参考文献  (6)
节点文献
引证文献  (0)
同被引文献  (0)
二级引证文献  (0)
1984(1)
  • 参考文献(0)
  • 二级参考文献(1)
1986(1)
  • 参考文献(0)
  • 二级参考文献(1)
1999(1)
  • 参考文献(0)
  • 二级参考文献(1)
2002(2)
  • 参考文献(0)
  • 二级参考文献(2)
2003(1)
  • 参考文献(0)
  • 二级参考文献(1)
2005(2)
  • 参考文献(0)
  • 二级参考文献(2)
2006(4)
  • 参考文献(1)
  • 二级参考文献(3)
2007(3)
  • 参考文献(0)
  • 二级参考文献(3)
2008(2)
  • 参考文献(0)
  • 二级参考文献(2)
2009(1)
  • 参考文献(0)
  • 二级参考文献(1)
2010(1)
  • 参考文献(1)
  • 二级参考文献(0)
2011(4)
  • 参考文献(1)
  • 二级参考文献(3)
2013(2)
  • 参考文献(0)
  • 二级参考文献(2)
2015(3)
  • 参考文献(0)
  • 二级参考文献(3)
2016(3)
  • 参考文献(1)
  • 二级参考文献(2)
2017(2)
  • 参考文献(1)
  • 二级参考文献(1)
2018(1)
  • 参考文献(1)
  • 二级参考文献(0)
2020(0)
  • 参考文献(0)
  • 二级参考文献(0)
  • 引证文献(0)
  • 二级引证文献(0)
研究主题发展历程
节点文献
联锁软件
形式化验证
模型检验
安全需求
研究起点
研究来源
研究分支
研究去脉
引文网络交叉学科
相关学者/机构
期刊影响力
铁道通信信号
月刊
1000-7458
11-1975/U
大16开
北京市海淀区大柳树路2号
2-403
1957
chi
出版文献量(篇)
8402
总下载数(次)
29
论文1v1指导