摘要
C3高铁动车组利用普速线迂回运行系统（简称CTCS-1级列控系统）是为了支持高铁线路故障后动车组能够在普速线路上运行而设计的一套全新的系统，该系统在尽量减少对普速线路上既有设备改造的前提下，把普速线路上广泛使用的CTCS-0级列控系统改造成CTCS-1级列控系统，既解决了普速线路存在的安全相关问题，又保证了动车组在普速线路上的安全高效运行。该系统的技术方案目前处在研究阶段，车站数据服务器（SDS）作为该系统地面的核心设备，将生成的无线报文通过无线广播通信方式发送给车载设备，对SDS进行建模验证与实现可以降低开发成本和开发风险，促进CTCS-1级列控系统方案的完善。 论文基于SCADE完成对SDS的建模验证与实现。论文完成的主要工作如下： （1）研究基于SCADE的软件开发方法，并提出基于SCADE的SDS总体研究方案，该研究方案包括SDS功能需求分析、SDS参与的关键场景建模验证、SDS功能详细设计、SDS功能建模验证与实现等内容。 （2）SDS功能需求分析。通过梳理CTCS-1级列控系统总体技术规范文档中与SDS相关的内容，分析SDS的交互功能需求和内部功能需求，把SDS的功能细化为系统自检模块、数据配置模块、动态数据管理模块、无线报文发送模块、状态监测和记录模块。在分析SDS功能需求的过程中，发现SDS与列车通信时采用无线单向广播方式，在现有的列控系统中从未使用过，所以需要从SDS参与的场景中选取无线广播通信场景进行深入研究。 （3）SDS参与的关键场景——无线广播通信场景的建模验证。通过分析CTCS-1级列控系统的总体技术规范、无线广播通信场景的需求，对无线广播通信场景进行详细设计。采用SysML语言对场景建模，通过设计的SysML-PRISM模型的转换算法将其转换为PRISM模型，并在概率模型检验工具PRISM中进行模型验证，证明了场景设计的合理性以及无线单向广播通信方式的可行性，确定了场景相关的技术指标，作为后续研究的基础。 （4）SDS功能建模验证与实现。依据分析的SDS的功能需求，完成SDS每个功能模块的详细设计、SCADE模型设计，结合研究无线广播通信场景时确定好的场景相关技术指标，完善建立的每个功能模块的SCADE模型，把各个功能模块集成在一起构成SDS的SCADE模型。通过SCADE仿真验证工具进行SDS的SCADE模型的仿真、覆盖率分析，验证模型的正确性和仿真的完备性。采用形式化验证方法证明所建的SDS的模型是满足安全属性的，保证了SDS的安全性。采用代码生成器KCG自动生成面向工程的C代码，把C代码放到目标机中联调联试，验证了设计的SDS模型满足预期的功能要求，以及用SCADE开发SDS系统的可行性。
NETL