期刊文献+
共找到3篇文章
< 1 >
每页显示 20 50 100
基于UPPAAL的城市轨道交通CBTC区域控制子系统建模与验证 被引量:15
1
作者 吕继东 唐涛 +1 位作者 燕飞 徐天华 《铁道学报》 EI CAS CSCD 北大核心 2009年第3期59-64,共6页
CBTC(Communication Based Train Control)系统可有效提高轨道交通的列车运营效率,降低系统建设和维护费用。在系统研发过程中需对系统进行建模、仿真和验证,发现系统设计缺陷,以保证系统的安全性。CBTC区域控制子系统是一实时控制系统... CBTC(Communication Based Train Control)系统可有效提高轨道交通的列车运营效率,降低系统建设和维护费用。在系统研发过程中需对系统进行建模、仿真和验证,发现系统设计缺陷,以保证系统的安全性。CBTC区域控制子系统是一实时控制系统,它要求控制时间的精确性和控制过程的准确性。本文通过分析城市轨道交通CBTC区域控制子系统的结构,给出满足该子系统安全性的功能和性能要求,并结合时间自动机理论方法提出包含列车、速度距离控制器、区域控制器和多车控制队列的时间自动机网络模型。同时,应用UPPAAL验证工具对CBTC区域控制子系统进行仿真建模,并验证该子系统功能和性能要求,从而保证了系统模型的安全性和受限活性。 展开更多
关键词 区域控制子系统 UPPAAL 时间自动机 自动验证
在线阅读 下载PDF
ATP国产化开发项目区域控制中心子系统
2
作者 黄蔚 《铁路通信信号信息》 2002年第4期5-9,共5页
关键词 ATP国产化 开发 区域控制中心子系统 地铁 信号系统
在线阅读 下载PDF
基于混成自动机的城市轨道交通ZC子系统建模与验证方法 被引量:6
3
作者 黄友能 张鹏基 +1 位作者 侯晓鹏 唐涛 《中国铁道科学》 EI CAS CSCD 北大核心 2016年第2期114-121,共8页
结合城市轨道交通列车控制系统区域控制器(ZC)子系统的混成特性,采用扩展的统一建模语言(UML)建立ZC子系统的UML顺序图;采用模型转换方法,提出从源模型到目标模型转换的定义和规则,将ZC子系统的UML顺序图转换为形式化的线性混成自动机模... 结合城市轨道交通列车控制系统区域控制器(ZC)子系统的混成特性,采用扩展的统一建模语言(UML)建立ZC子系统的UML顺序图;采用模型转换方法,提出从源模型到目标模型转换的定义和规则,将ZC子系统的UML顺序图转换为形式化的线性混成自动机模型,用于ZC子系统功能的安全验证。以北京地铁亦庄线ZC边界切换控制功能场景为例,建立该场景的UML顺序图;将其对应车地通信的5个阶段细分为5个组合片段;根据模型转换定义及规则,将各组合片段转换为线性混成自动机,进一步将不同组合片段的线性混成自动机合成完整的目标线性混成自动机;根据建立的线性混成自动机模型,采用验证工具BACH对该场景的7条功能性质和4条安全性质进行验证。结果表明:ZC边界切换控制功能满足设计需求,列车能够安全通过地面区域边界点,没有超速情况且能够在接管ZC管辖范围内安全停车。表明所提出的建模和验证方法是可行的,弥补了对具有混成特性列车控制系统既有验证方法的不足。 展开更多
关键词 列车控制系统 区域控制子系统 系统建模 系统功能 安全验证
在线阅读 下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部