基于混成自动机的城市轨道交通ZC子系统建模与验证方法

• 作者: 侯晓鹏 唐涛 张鹏基 黄友能
• 来源期刊: 中国铁道科学
• 学科: 交通运输
• 关键词: 列车控制系统 区域控制器子系统 系统建模 系统功能 安全验证
• 年，卷（期）: 2016,（2）
• 页码范围: 114-121
• 页数: 8页
• 分类号: U285.21
• 字数: 6574字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-4632.2016.02.16

摘要

结合城市轨道交通列车控制系统区域控制器(ZC)子系统的混成特性,采用扩展的统一建模语言(UML)建立ZC子系统的UML顺序图;采用模型转换方法,提出从源模型到目标模型转换的定义和规则,将ZC子系统的UML顺序图转换为形式化的线性混成自动机模型,用于ZC子系统功能的安全验证.以北京地铁亦庄线ZC边界切换控制功能场景为例,建立该场景的UML顺序图;将其对应车地通信的5个阶段细分为5个组合片段;根据模型转换定义及规则,将各组合片段转换为线性混成自动机,进一步将不同组合片段的线性混成自动机合成完整的目标线性混成自动机;根据建立的线性混成自动机模型,采用验证工具BACH对该场景的7条功能性质和4条安全性质进行验证.结果表明:ZC边界切换控制功能满足设计需求,列车能够安全通过地面区域边界点,没有超速情况且能够在接管ZC管辖范围内安全停车.表明所提出的建模和验证方法是可行的,弥补了对具有混成特性列车控制系统既有验证方法的不足.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学电子信息工程学院	152	2578	27.0	40.0
2	黄友能	北京交通大学电子信息工程学院	17	105	7.0	10.0
6	张鹏基	北京交通大学电子信息工程学院	1	8	1.0	1.0
7	侯晓鹏	北京交通大学电子信息工程学院	1	8	1.0	1.0