• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Conference on Sensors and Materials Manufacturing Science >Automatic Conversion Method of the requirements specification verification for CTCS Level 3
【24h】

Automatic Conversion Method of the requirements specification verification for CTCS Level 3

机译：CTCS等级3的要求规范验证的自动转换方法

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Chinese Train Control System Level 3(CTCS-3) is a typical complex cyber-physical system which connects the control center, the station and the train. In order to ensure the friendly communication between the different manufacturers' equipment, the high reliability is required by the CTCS-3 system. The reliability of a system can be tested with the formal verification method and a lot of formal tools have been developed, such as SPIN, VIS and NuSMV. In this paper, we describe the modeling techniques and abstractions of the control process. The required assembly unit has been specified as extended class. The required behavior has been specified as extended state machine diagrams and translated to temporal logic properties. Then, we propose a method to simplify the steps which transfer a UML model into a formal model. Moreover, the transition can be implemented with development language, where its result-the formal model-can be run by the formal tool and return an analysis result. At last, we take the Radio Block Center (RBC) Handover of CTCS-3 as an example, and the experimental results show the validity and feasibility of this method.
机译：中国火车控制系统级别3（CTCS-3）是一个典型的复杂网络物理系统，可连接控制中心，车站和火车。为了确保不同制造商设备之间的友好沟通，CTCS-3系统需要高可靠性。可以使用正式验证方法测试系统的可靠性，并且已经开发了许多正式工具，例如旋转，VIS和NUSMV。在本文中，我们描述了控制过程的建模技术和抽象。所需的装配单元已被指定为扩展类。所需的行为已指定为扩展状态机图并转换为时间逻辑属性。然后，我们提出了一种简化将UML模型传输到正式模型的步骤的方法。此外，转换可以用开发语言实现，其中它的结果 - 正式模型 - 可以由正式工具运行并返回分析结果。最后，我们以CTCS-3的无线电块中心（RBC）切换为例，实验结果表明了该方法的有效性和可行性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号