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

• 作者: 水晶 董昱 黎磊
• 来源期刊: 计算机工程
• 学科: 地球科学
• 关键词: 列控系统 符号模型检验 形式化方法 车载设备 模式转换
• 年，卷（期）: 2013,（3）
• 所属期刊栏目: 轨道交通专题
• 页码范围: 12-15
• 页数: 4页
• 分类号: N945
• 字数: 2821字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2013.03.003

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	董昱	兰州交通大学自动化与电气工程学院	75	556	12.0	19.0
2	水晶	兰州交通大学自动化与电气工程学院	1	6	1.0	1.0
3	黎磊	兰州交通大学自动化与电气工程学院	3	8	1.0	2.0