应用ETDFA生成CBTC联锁软件形式化模型的方法

• 作者: 郑鸿昌 陈启香 高雪娟
• 来源期刊: 计算机测量与控制
• 关键词: CBTC 联锁软件 ETDFA 形式化方法
• 年，卷（期）: 2017,（12）
• 所属期刊栏目: 测试软件工程
• 页码范围: 120-124,136
• 页数: 6页
• 分类号: TP273
• 语种: 中文
• DOI: 10.16526/j.cnki.11-4762/tp.2017.12.032

摘要

CBTC系统的联锁软件为SIL4级的高安全、高可靠软件,目前广泛使用的软件测试和仿真验证的结果严重依赖选取的测试向量,要保证高覆盖率的测试十分困难;EN50128中强烈推荐SIL4等级的软件使用形式化方法完成软件需求规格说明书和软件设计,因此,采用形式化的方法设计软件,是构造高可靠、高安全软件的一个重要途径;总结了现有的CBTC系统中联锁子系统集成方式及优缺点,并使用事件确定有限自动机ETDFA (event deterministic finite automata)模型对适用性更优的升级型集成方式的联锁软件的联锁逻辑完成形式化定义,保证联锁逻辑的正确性,减少软件的不确定性描述;以办理进路为例生成联锁对象的ETDFA模型,验证该方法的有效性和可行性;该方法不仅为CBTC联锁软件的设计与开发提供新思路,而且有助于安全苛求软件的形式化验证与分析,提高联锁软件的安全性和正确性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈启香	宝鸡文理学院电子电气工程学院	9	5	1.0	1.0
2	高雪娟	株洲中车时代电气股份有限公司通信信号事业部	1	1	1.0	1.0
3	郑鸿昌	株洲中车时代电气股份有限公司通信信号事业部	1	1	1.0	1.0