一种基于场景的CTCS-3列车控制系统建模方法研究  

A Kind of Modeling Method for CTCS-3 Based on Operation Scenario

作　　者：王帅[1,2] 吉吟东[2,3] 杨士元[3] 

机构地区：[1]清华大学计算机科学与技术系,北京100084 [2]清华信息科学与技术国家实验室,北京100084 [3]清华大学自动化系,北京100084

出　　处：《铁道学报》2011年第9期55-61,共7页Journal of the China Railway Society

基　　金：国家科技支撑计划(2009BAG12A08);铁道部科技研究开发计划(2009X003-B)

摘　　要：对CTCS-3列车控制系统进行有效的测试、分析和验证是保证列车运行安全和旅客生命财产安全的重要手段,而形式化模型是系统测试、分析和验证的基础。本文以CTCS-3列车运行控制系统的UML非形式化模型为基础,以自动机模型作为系统形式化模型描述的数学工具,研究UML顺序图(场景)自动转化为自动机网模型的方法。首先将场景的UML顺序图自动转化为子系统的子自动机模型,然后通过合并不同场景的子自动机模型,得到子系统的组元自动机模型,最后通过对通信通道的建模得到系统的自动机网模型。使用本方法,基于系统的UML顺序图模型可以自动生成系统的自动机网模型。Test, analysis and verification of China train control system level 3 （CTCS-3） are important ways to ensure the safety of train running and people lives. Especially, the formalized model is the foundation of these work. In this paper, we use the automata net to model the CTCS-3. The method transforming the sequence charts into the automata net model is studied. The sequence charts of the system firstly are transformed into the sub-automata of each sub-system, and then the sub-automata are combined into the automata model for the each sub-system. At last, the automata net model is constructed for the system after modeling the communication channels between each two sub-systems. The sequence charts of the system are transformed into the automata net model of the system automatically through using our method.

关 键 词：CTCS-3列车运行控制系统 自动机 顺序图 形式化建模 运营场景 

分 类 号：U283[交通运输工程—交通信息工程及控制] TP301[交通运输工程—道路与铁道工程]