• 查询稿件
  • 获取最新论文
  • 知晓行业信息
张越, 王海峰. 基于Event-B的计算机联锁安全规范描述与验证[J]. 铁路计算机应用, 2013, 22(11): 47.
引用本文: 张越, 王海峰. 基于Event-B的计算机联锁安全规范描述与验证[J]. 铁路计算机应用, 2013, 22(11): 47.
ZHANG Yue, WANG Haifeng. Specification description and verification of computer interlocking safety based on Event-B[J]. Railway Computer Application, 2013, 22(11): 47.
Citation: ZHANG Yue, WANG Haifeng. Specification description and verification of computer interlocking safety based on Event-B[J]. Railway Computer Application, 2013, 22(11): 47.

基于Event-B的计算机联锁安全规范描述与验证

Specification description and verification of computer interlocking safety based on Event-B

  • 摘要: 本文结合具体的站场实例,基于Event-B方法对信号开放、道岔控制、进路解锁等联锁系统关键安全规范进行了形式化模型描述和验证分析,给出了严格的分析结果.工作表明,铁路信号联锁系统是具有复杂时序逻辑的控制系统,Event-B方法适合于该类系统的描述与验证.通过形式化的联锁安全规范描述与验证,可以在系统开发的早期及时发现设计错误或漏洞,有助于提高计算机联锁系统的软件开发质量.

     

/

返回文章
返回