通用型列控系统的安全计算机设计与验证

石婷婷

（江西省电子信息技师学院，江西南昌330096）



通用型列控系统的安全计算机设计与验证

石婷婷

（江西省电子信息技师学院，江西南昌330096）

介绍了现代列车运行系统对计算机依赖程度在不断提高，分析了在对控制列车运行系统的安全计算机进行设计活动时，需对计算机硬件结构进行优化，实现其安全性的提高；同时需将空间运算与时间运算结合起来，让仿真模拟计算能够落实到位。

列车运行；安全计算机；设计与完善；平台控制

引言

随着人们生活水平不断提高，人们生活对于现代科技的运用方式与需求也在不断提高。当计算机技术与其它技术进行结合时，能实现诸多行业的科技发展，这为提高社会大众生活质量，促进社会进一步发展等都有着积极影响。当计算机系统能够让独立的结构转化为IMA结构时，这样综合化的平台给信息传递创造了前所未有的良好环境，进而为信息活动传输精简化、便捷化提供了技术支持，也为轨道交通运输的信息传递提供了物质保障。

1　对计算机系统硬件结构的创新改进

在一般情况下，信号系统指的是地面指挥系统以及列车的车载系统，车载的设备是在安全计算机展开的基础上来完成相关控制活动的。在地面指挥系统中，其所构建的是一个基于计算机设备才能完成各项任务的复杂系统，具备着一定的典型性。在研究其主要的运行模式是借助于CTCS-3系统，将这个所制定的方案做简化且富有实践使用价值。同时，这个方案的开展平台也具备着极高适应能力，可以广泛地被运用与车载信号系统之中。

在对分布原则进行遵守的前提下，将CTCS-3这一信号系统进行划分，使得核心主机得以借助外部远程系统组合。在核心的主机系统中，将安全计算机平台进行建立，将其放置在机械室的内部。它可做到无线闭塞的传播以及临时的信息处理，同时，对计算机联锁的把控与列车整体控制都有着一定积极影响，使得列车整体控制活动得以顺利落实到位。当然，在对远程的外设部分进行设置时，需做到尽量精准控制，确保远程控制活动能够准确做到对“控制对象”的控制，最大程度地减少连线距离。

2　对UM L模型的运用与验证

2.1对建模活动的控制性进行明确

就列车的车载设备安全系统来说，其分为了四级的安全级别，其根据国际标准所进行设计活动是对这些标准的明确追求，这也是对形式化方法的分析与表现。形式化方法指的是对数学逻辑运用得以做到描述、检测系统的表现形式。同时，也需要对这个方式的运用来满足相关设计活动的开展，进而达到预期的设定需求。由于在计算机系统中，对于对象处理是在统一化的建模语言影响下所开展的活动，它易于表达，且表述活动较为直观，进而让各类图形、信息可以较为直观地得以表现，是静态结构与动态表现的主要表现形式。所以，UML这一建模系统得到了广泛运用。

除此之外，由美国研发的检测工具SMV也是目前得到行业内部普遍认可的检测方式。就其工作原理来说，它主要借助于对有穷状态下的模型特征进行分析与探究，进而完成对整个状态空间的“查缺补漏”。这个检测活动在工业应用中取得了诸多的成就。

2.2建模活动的开展流程

将UML这一建模系统的语言与符号进行结合，进而完成对系统运行活动的明确，就其开展流程来说，主要分为以下内容：对需求明确进而完成UML这一模型的建立，使得其与设定方案一致；将需要验证的系统进行抽象化处理，使得其形成一个可控的模型，将所拓展的抽象图形建立与探究，达到对其可行性的测试；完成对转换规则的建立与完善，将需要验证活动的部分进行逻辑公式的表达，将其转换为NuSMV模型；借助于对检验工具的使用让存在的漏洞与失误得以一一明确，做到及时处理。

3　对列车车载设备的建模活动

3.1UML的模式转换活动

将系统的需求建立成一个UML的模型，进而完成对工作环境的真实还原，这样一来，可以使还处于研发状态的系统能够得到进一步完善，它与前期的设计对比活动不同，这个活动的开展价值在于其独特的适应性能够让所有急需解决的问题得以顺利地被发现、处理。这样的设计优势存在可以让整个解决方案的制定更好地被适用。因此，在前期的建模活动中，其检测的内容，一方面是对系统的抽象表达内容的追求，另一方面，也要对系统内部的具体细节进行思考，使得那些难以被检测活动发现的属性漏洞得以弥补。在这个模式的转化过程中，车载设备需要将列车控制平台、答复器等设备进行结合，做到信息的及时交换。由此可见这样的交换活动待遇有一定的额抽象性与开展难度。同时，就类图的类型来说，可以分为：中心类、车载设备类、列车类以及答复器类等形式。这样的构图活动让转化、建模等设计需求得以满足，同时，也让原本抽象化的信息得以具体化的表现。

3.2对设备转换形式的验证与表现

就SMV这一检测系统来说，其属性中对于定义的制定，需要对CTL这一公式进行利用，进而让SPEC来作说明。当SMV工具处于运行状态下的时候，它如果可以满足CTL的开展需求，则让SMV的输出结果表现为true；当其不满足的时候，就需要将这些错误的漏洞进行一一明确与纠正，然后再进行相关的验证。做到对UML拓展运用，将其转化使得这一模型得以多样化地被组成。其中，主模块作为系统的主要组成部分，需要满足系统的功能需求，子模块需要将验证的性质进行追求，让其每个部分进行对应，借此来完成转换活动。

3.3对模型所得结果的验证探究

模型的验证结果需要做到安全性、灵活性以及可达性。要达到这三方面，具体如下：1）对安全性的保障。在计算机系统中，安全性即是计算机在运行的过程中，可以完成对各类影响因素的处理，其表达式SPECAG表示的是当CTCS-2作为列车控制系统的时候，如若，其不能做到对信息的有效答复，即需要在安全监控活动的影响下，来完成对监控模式的外部控制，借助于对表达式的验证，如果是true，则能够证明这一系统的运行具备安全性的保障。2）对灵活性的探究。对验证活动的开展需要满足验证表达式。同时，在系统中，无论是怎样的模式都能灵活地进行转化与隔离。这一表达式的结果是对模式灵活性的明确。3）对可达性的追求。表达式作为SPEC EF的验证需求表现，其在系统中的状态将会直接影响到转换活动开展。如果，存在的系统不能达到这一需求，则说明这一系统存在运行的缺陷，需求对其进行明确与处理；但是，当这样的状态不存在时，则表明该模型不存在问题，进而保障其可达性的实现。

［1］蔡旭.LKD2-T2型列控系统升级改造实施与应用［J］.上海铁道科技，2013（2）：58-60.

［2］郑升，曹源，张玉琢，等.通用型列控系统的安全计算机设计与验证［J］.北京交通大学学报，2014（3）：128-134.

（编辑：姚欢）

Computer Design and Safety Verification Universal Train Control System

Shi Tingting
（Jiangxi Electronic Inform ation Technician College，Nanchang Jiangxi 330096）

Modern train operation system depending on the computer is increasing.To control the safety of train operation system is analyzed in the computer to carry on the design activities，to optimize the hardware structure，realize the improvement of its safety；At the same time，the space and time calculations must be combined，which makes simulation calculation put in place.

train；computer security；design and perfect；platform control

TP302

A

2095-0748（2015）23-0094-02

10.16525/j.cnki.14-1362/n.2015.23.43

2015-11-04

石婷婷（1986—），女，江西南昌人，本科，助理讲师，研究方向：软件工程。