基于通信顺序进程与B方法的CBTC计算机联锁系统的形式化建模与验证

• 作者: 王鲲
• 来源期刊: 中国铁道科学
• 学科: 交通运输
• 关键词: 城市轨道交通 CBTC 计算机联锁系统 形式化方法 通信顺序进程 B方法
• 年，卷（期）: 2018,（3）
• 页码范围: 101-109
• 页数: 9页
• 分类号: U284
• 字数: 6746字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-4632.2018.03.14

摘要

针对CBTC联锁系统的复杂性,提出一种基于通信顺序进程(CSP)与B方法集成的形式化方法,即在通信顺序进程的通信事件与B方法抽象机的操作之间建立起一对一的映射关系,实现通信事件通过控制抽象机的操作、进而影响抽象机状态的目标,从而实现通信顺序进程和B方法之间的同步.以1个实际站场为例,采用B方法对具有复杂状态空间的CBTC联锁系统的逻辑状态运算建立抽象机,采用通信顺序进程对CBTC联锁系统与外部系统的并发交互行为建立进程,并通过映射关系使CBTC联锁系统的抽象机与外部交互行为进程同步,由此建立基于通信顺序进程与B方法的CBTC联锁系统的形式化模型.采用ProB工具对建立的CBTC联锁系统模型的安全性、无死锁性进行验证.发现并修改模型中的不一致、不完全、歧义等错误,从而验证了CBTC联锁系统的安全性和无死锁性,保证了系统的最终实现.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王鲲	中国铁道科学研究院通信信号研究所	14	49	5.0	6.0