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

对CTCS-3列车控制系统进行有效的测试、分析和验证是保证列车运行安全和旅客生命财产安全的重要手段,而形式化模型是系统测试、分析和验证的基础。本文以CTCS-3列车运行控制系统的UML非形式化模型为基础,以自动机模型作为系统形式化模型描述的数学工具,研究UML顺序图(场景)自动转化为自动机网模型的方法。首先将场景的UML顺序图自动转化为子系统的子自动机模型,然后通过合并不同场景的子自动机模型,得到子系统的组元自动机模型,最后通过对通信通道的建模得到系统的自动机网模型。使用本方法,基于系统的UML顺序图模型可以自动生成系统的自动机网模型。

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

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.