检索
E-mail
RSS
作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2013, Vol. 39 ›› Issue (3): 12-15.doi: 10.3969/j.issn.1000-3428.2013.03.003

所属专题： 智能交通专题

• 轨道交通专题 • 上一篇    下一篇

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

董 昱，水 晶，黎 磊   

  1. (兰州交通大学自动化与电气工程学院，兰州 730070)
  • 收稿日期:2012-06-25 出版日期:2013-03-15 发布日期:2013-03-13
  • 作者简介:董 昱(1962－)，男，教授，主研方向：铁道通信信号处理；水 晶、黎 磊，硕士研究生
  • 基金项目:
    国家自然科学基金资助项目(61164010)；甘肃省教育厅硕导基金资助项目(210110)

Formal Modeling and Verification of CTCS-2 Train Control System

DONG Yu, SHUI Jing, LI Lei   

  1. (School of Automation and Electrical Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China)
  • Received:2012-06-25 Online:2013-03-15 Published:2013-03-13

PDF

918

被引次数

1 | 1

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

关键词: 列控系统, 符号模型检验, 形式化方法, 车载设备, 模式转换

Abstract: For the designing complexity of CTCS-2 system, this paper proposes the method combining Unified Modeling Language(UML) and Symbolic Model Checking(SMC) for modeling and formal verification. It analyzes the mode conversion scene of CTCS-2 on-board equipment. The mode conversion scene of CTCS-2 on-board equipment is modeled by using the UML, and UML class diagrams and UML state diagrams are gotten as well, through formulating some exchanging rules to extend and abstract UML model and exchanging it to the NuSMV model. The property of to be verified system and system Symbolic Model Verifier(SMV) model are inputted to symbolic model verifier to check. The verified results are true, and it shows that mode conversion scene of CTCS-2 on-board equipment has activity, accessibility and security.

Key words: train control system, Symbolic Model Checking(SMC), formal method, on-board equipment, mode conversion

中图分类号: