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

第 33卷第 9期 铁 道 学 报 Vo1．33 No．9 2011年 9月 J()URNAI OFTHECHINA RAILW AY SOCIETY September 2011 文章编号 2011)09—0055—07 一 种基于场景的CTCS-3列车 控制系统建模方法研究 王 帅 ， 吉吟东。， 杨士元 (1．清华大学 计算机科学与技术系 ，北京 100084； 2．清华信息科学与技术 国家实验室，北京 i00084；3．清华大学 自动化系，北京 100084) 摘 要 ：对 CTcS一3列车控制系统进行有效 的测试 、分析和验证是保证列车运行安全和旅客生命财产安全 的重 要手段 ，而形式化模型是系统测试 、分析和验证 的基础。本文以 CTCS-3列车运行控制系统 的UMI非形式化模 型为基础 ，以自动机模 型作为系统形式化模 型描述的数学工具 ，研究 UML顺序 图(场景)自动转化为 自动机网模 型的方法 。首先将场景的UMI顺序 图自动转化为子系统的子 自动机模型，然后通过合并不 同场景的子 自动机 模型 ，得到子系统的组元 自动机模型，最后通过对通信通道 的建模得到系统的 自动机 网模型。使用本方法 ，基于 系统的UML顺序图模型可以自动生成系统的自动机网模型。 关键字：CTCS一3列车运行控制系统；自动机 ；顺序图；形式化建模 ；运营场景 中图分类号 ：U283；TP301 文献标志码 ：A doi：10．3969／i．issn．1。(]1一8360．2011．09．010 ． A KindofM odelingM ethod forCTCS一3 Basedon Operation Scenario WANG Shuai一， JIYin—dong。～， YANG Shi—yuan。 (1．DepartmentSchoolofComputerScience Technology ，TsinghuaUniversity，Beiiing100084，China 2．TsinghuaNationalLaboratoryforInformationScienceandTechnology，Beiiing100084，China； 3．DepartmentofAutomation，TsinghuaUniversity，Beijing100084，China) Abstract：Test，analysisandverificationofChinatraincontro1system leve13 (CTCS一3)areimportantwavsto ensurethesafetyoftrainrunningandpeoplelives．Especially，theformalizedmodelisthefoundationofthese work．Inthispaper，weusetheautomatanettomodeltheCTCS一3 Themethod transform ing thesequence