【摘要】铁路信号系统属于安全关键系统所谓安全关键系统是指系统的失效往往引起重大的生命、财产损失的系统。近年来由于计算机在铁路信号领域的广泛应用，并且随着硬件可靠性的提高，实现各种复杂功能的软件质量对系统的安全性影响随之增大提高软件可靠性和安全性成为开发安全关键系统的聚焦点软件开发过程就是把现实世界的需求反映成软件的模型化过程由于软件系统的大规模化、复杂化，需求变更频繁，使得模型化过程越来越困难，目前解决这种困难的方法之一是需求的形式化描述.
【关键词】形式；铁路；信号
铁路信号系统属于安全关键系统所谓安全关键系统是指系统的失效往往引起重大的生命、财产损失的系统。近年来由于计算机在铁路信号领域的广泛应用，并且随着硬件可靠性的提高，实现各种复杂功能的软件质量对系统的安全性影响随之增大提高软件可靠性和安全性成为开发安全关键系统的聚焦点软件开发过程就是把现实世界的需求反映成软件的模型化过程由于软件系统的大规模化、复杂化，需求变更频繁，使得模型化过程越来越困难，目前解决这种困难的方法之一是需求的形式化描述.
形式化方法已经研究和应用了大约30年，和其他人用来表示程序语义.形式化方法是基于离散数学和形式逻辑的一种方法它以一定的数学概念和理论为基础，具有明确的、无二义性的语法和语义形式化语言的外在特点是：代替日常语言的词汇，引进了构成这些语言字母的专门符号，以紧凑性和可观察性为特色；在这些语言中不仅提供了原始标志（语言字母），而且准确鲜明地定义了建立名称和含义表述的规则，定义了把一些表述（判断、公式等符号系列）变成另一种表述的规则由于形式化语言从类型上说基本上是描述性和断定性而非评论性的，在描述性语言中又以分析陈述为主，因此，它能够表达深刻复杂的内容并进行演算化推理形式化方法的优点之一是它对设计产生的错误有一定的避错作用，其离散性和形式逻辑性分别适合于软件的特性和系统的设计与证明首先，形式化方法能避免二义性，系统需求分析和各种文档说明的二义性是设计型故障的主要来源之一；其次，形式化方法比传统方法更加完整、周密形式逻辑在设计中的应用，使设计和证明按一条条逻辑线路进行，避免了逻辑上的混乱本文主要阐述在铁路信号域中形式化方法应用的研究内容，铁路信号领域知识的形式化表达的实现.
1.铁路信号系统及其知识形式化表示
1.1铁路信号域知识
铁路信号是一个有名论域按传统的方法，铁路信号可被划分为车站、区间、编组站调车和调度集中四大子系统在国内，目前主要应用于城市轨道交通的列车自动控制系统亦可作为铁路信号的一个子域随着铁路信号技术的发展，目前已有人提出铁路网络信号学的概念，因而铁路信号域知识随着科学技术的发展而不断更新、拓展世界各先进国家自上世纪 年代开始较早地将计算机应用于车站信号自动控制子系统，这些成果主要体现在铁路车站计算机联锁系统上而近年来其他三大子系统中，计算机的应用也日益增多对铁路信号域知识形式化表示的目标，是使人们能借助于人工智能的理论和方法，去解决因计算机在铁路信号领域中的广泛应用而引出的许多问题如：操作控制数据的自动生成，联锁表的自动生成，联锁软件的计算机辅助设计，列车和车列的运行仿真等等.
1.2铁路计算机信号系统
尽管铁路信号控制包括多个子系统，但在一个调度区段内与列车运行紧密相关的主要是车站联锁和区间闭塞两大部分车站联锁系统是以计算机、现代通信等技术手段实现以进路控制为主要内容的联锁系统，它以色灯信号机、动力转辙机和轨道电路作为室外三大基础设备基础设备的作用是执行行车指挥的命令，而保证行车安全和提高作业效率通过联锁软件来实现区间闭塞系统是为了保证区间内列车行车安全及提高区间通过能力的安全系统区间的通过信号随着列车的运行自动转换，同时相邻车站的进站信号变化也影响分区信号显示根据系统各主要部分的功能分工和设置地点的不同，两系统可表示成一个层次结构.
1.3铁路信号计算机系统的形式化表示方法
本文的形式化研究主要是指在控制层中对相关对象以及它们相互关系的表达知识的表示是对知识进行概括，形成概念并建立起各种关系，用适合于计算机表示和处理的方法描述出来过去铁路信号各对象之间的逻辑关系的处理主要是采用继电器接点电路来实现的由于继电器的体积、能耗以及维修等方面的开销，势必要从逻辑功能上退出，而仅承担功能开关的作用，因此需要研究一种适用于计算机处理的铁路信号知识表达方式知识表达主要包含知识的内涵和知识的关系两方面内容，此外还有与它们相联系的知识处理的规则.
我国铁路信号系统以往的开发方式大多是基于技术规范的，在保障系统安全性、可靠性方面起到了积极的作用.然而随着高速铁路的发展和微电子、计算机、通信等现代信息技术的广泛应用，以及我国铁路信号产品走向国际化需求的增大，传统的开发方式在保障电气/电子/可编程电子安全相关系统的安全性方面，与国际盛行的安全保障、评估理论和技术相比存在一定的差距.
1.3.1知识的内涵表示
铁路车站及区间信号布置平面图、基本规则库以及区域性数据等构成了铁路信号域的基本知识知识库由单元库和规则库两部分构成，如图所示其中单元库包括单元图形库和结构库，存放与铁路现场相对应的拓扑图形和结构；规则库存放的是由铁路信号域的基本原理、定理和规定等知识导出的规则处理模块根据知识库中的知识进行处理，实现功能.
在构建铁路信号域知识库时，采用了面向对象的方法，把描述求解问题的属性概念（知识）和智能行为（知识处理方法）模型化为对象，成为知识库中的一个独立知识单元，称为对象（类）在此知识库中，知识类型包括事实、规则和过程三种每个对象包含其中的 种知识类型事实知识有抽象和实例两种不同的类别，描述如下抽象知识：<类名><超类名><类说明>。
基本规则是铁路信号计算机系统必须遵循的准则首先将经验知识整理成断言形式，然后再从断言变成规则.在这里使用一阶谓词逻辑来形式化表达系统的基本准则.
1.3.2知识的关系表达
对铁路信号系统进行形式化表达的关键在于是否有一系列的抽象化模型，很重要的一条是摆脱继电器网络形式信号电路的约束，要求以数据库为基础的更一般的表达数据库的构建实质是用高度的抽象来模型化系统，将信号系统中的变量转化为若干基本的变量———信号机、道岔和区段作为低层层次进路作为一种高层次的变量，它是指以限界为横截面，以所有区段总长为其长度，包含一定数量的信号机、道岔和区段的一段空间信号机、道岔、区段和进路之间存在着各种关系。
在确定了各变量之间的关系后，再来探索关系之间可能的运算和这些运算应遵循的规则，主要有自反、传递、交换、结合例如：进路的包容关系运算是自反的，传递的，不可交换的，可结合的；进路的接续关系运算是非自反的，非传递的，可交换的，可结合的。
2.结论
铁路信号作为一种安全关键系统，是形式化方法的重要应用领域.本文将形式化方法应用于铁路信号域，开发了铁路站场数据录入系统.它是铁路计算机联锁安全软件测试评估平台的一个子系统，成为软件测试中数据自动生成、操作命令及设备和运行仿真命令、测试案例等自动或半自动生成的基础.此系统已经成功地完成了数个车站的测试工作，验证了方法的正确性和有效性.而且这种形式化表示方法同样适用于铁路区间知识域，目前正应用于开发铁路区间计算机控制信号系统测试评估平台.显然，随着铁路信号域知识的扩充，知识库也需要不断地更新，铁路信号域的形式化表示仍是一个需要继续和深入研究的课题。
参考文献
[1]吴芳美.铁路安全软件测试评估[M].北京：中国铁道出版社，2009