CTCS-3级列控系统临时限速服务器建模与形式化验证

• 作者: 万勇兵 徐中伟 梅萌
• 来源期刊: 系统仿真学报
• 学科: 工学
• 关键词: 中国列车运行控制系统 临时限速服务器 消息顺序图 时间自动机 UPPAAL
• 年，卷（期）: 2013,（1）
• 所属期刊栏目: 复杂系统建模与仿真
• 页码范围: 132-138
• 分类号: TP391.9
• 语种: 中文

摘要

临时限速服务器是CTCS-3级列控系统的重要组成部分,其系统安全性直接影响到高速铁路的运营安全.在TSRS系统研发过程中需对系统进行仿真建模和验证,发现系统设计错误,以保证系统的安全性.分析CTCS-3级列控系统临时限速服务器的组成结构,提取系统功能和性能规范约束,利用消息顺序图对TSRS与外部系统之间的信息交互行为建模,并将系统MSC模型转化为UPPAAL中的时间自动机仿真模型,对系统的功能和性能要求进行形式化验证.验证结果确认了系统的安全性和受限活性,为进一步完善TSRS设计和系统开发提供参考.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐中伟	同济大学电子与信息工程学院	95	644	13.0	20.0
2	梅萌	同济大学电子与信息工程学院	21	89	4.0	9.0
3	万勇兵	同济大学电子与信息工程学院	5	46	4.0	5.0