CTCS-2级列控系统的形式化建模与验证

董昱; 水晶; 黎磊

首页> 中文期刊> 《计算机工程》 >CTCS-2级列控系统的形式化建模与验证

CTCS-2级列控系统的形式化建模与验证

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

团队文献服务 >>

页面导航

摘要
著录项
引文网络
相似文献
相关主题

摘要

由于CTCS-2级列控系统设计复杂,因此提出一种将统一建模语言(UML)与符号模型检验相结合的形式化建模与验证方法.分析CTCS-2级列控车载设备的模式转换场景,对其进行UML建模得到UML类图和状态图,制定转换规则对UML模型进行扩展和抽象,使其转化为NuSMV模型.将待验证的系统性质和转化后的检验程序输入符号模型检验系统进行验证,验证结果都为true,表明CTCS-2级列控车载设备的模式转化场景具有活性、可达性和安全性.

著录项

来源
《计算机工程》 |2013年第3期|12-15|共4页
作者
董昱; 水晶; 黎磊;
展开▼
作者单位

兰州交通大学自动化与电气工程学院;

兰州730070;

兰州交通大学自动化与电气工程学院;

兰州730070;

兰州交通大学自动化与电气工程学院;

兰州730070;

展开▼
原文格式 PDF
正文语种 chi
中图分类系统工程;
关键词
列控系统; 符号模型检验; 形式化方法; 车载设备; 模式转换;

相似文献

中文文献
外文文献
专利

1. CTCS-3级列控系统车地交互流程形式化建模与验证 [J] . 刘中田 ,吕继东 ,孙伟亮 . 北京交通大学学报 . 2011,第002期
2. CTCS-3级列控系统规范的建模与形式化验证方法研究 [J] . 谢雨飞 ,唐涛 ,徐田华 . 铁道学报 . 2011,第007期
3. CTCS-2级列控系统数字化验证平台研究 [J] . 张小舟 ,张亚东 ,郭进 . 铁道通信信号 . 2010,第012期
4. CTCS-3列控系统RBC切换的形式化建模、分析与验证 [J] . 潘登 ,郑应平 . 计算机应用研究 . 2013,第002期
5. 基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法 [J] . 吕继东 ,李开成 ,唐涛 . 中国铁道科学 . 2012,第005期
6. 既有线CTCS-2级列控系统规范及仿真测试系统——列控系统检测平台研究 [C] . 李辉 . 中国铁道科学研究院通信信号研究所（通号所）建所60周年学术报告会 . 2010
7. CTCS-3级列控系统等级转换场景形式化建模与验证 [A] . 宋丽梅 . 2018

CTCS-2级列控系统的形式化建模与验证

摘要

著录项

引文网络

相似文献

相关主题

期刊订阅