面向形式化验证的联锁翻译器软件设计

王绍新，王燕芩，闫连山

（1.卡斯柯信号（成都）有限公司，成都 610083；2．卡斯柯信号有限公司，上海 200071；3．西南交通大学信息科学与技术学院，成都 611756）

形式化证明是用数学方法去证明电子或者计算机系统是完备的、无漏洞的，在电子硬件设计和航天基建领域比较常用。铁路信号的根本功能是保障列车运行安全、提高运输效率，联锁系统是铁路信号的核心技术装备，它通过对信号机、道岔和进路的控制来指挥行车、防止列车冲突。在地铁调度领域，由巴黎地铁信号系统开始，在北美、欧洲、亚洲及南美洲的部分国家的地铁系统开发中，形式化证明方法已经被广泛使用。随着计算机联锁系统的应用推广，联锁系统对软件的依赖性越来越强，如何提高联锁软件的质量、确保系统安全是近年来轨道交通领域研究的热点问题。

1 联锁系统形式化验证

1.1 形式化在轨道交通领域的应用现状

形式化方法起源于20世纪60年代，在学术界已有很多成果，同时也发展出多个分支。由于其研发有一定的技术难度，前期的投入也比较大，因此在工业界的应用时间并不长。但是国外已经有一些完全使用形式化方法开发出的铁路信号系统，如巴黎地铁14号线的自动驾驶系统就是采用形式化方法开发的，至今未发现缺陷。

随着形式化方法的发展，各国铁路业主和信号厂商都已经开始关注并积极研究形式化方法应用于信号系统的开发或验证。国外业主方已经逐步将使用形式化方法开发或验证铁路信号系统作为一个强制的要求，如巴黎地铁(RATP)和纽约公共运输局（NYTC）、加太铁路（Canadian Pacific）、斯德哥尔摩地铁（Stockholm Metro）、比利时国家铁路（Infrabel）、瑞典铁路（Trafikverket）、英国的铁路网公司（Network Rail）等，在多个不同的项目中应用了形式化方法。

形式化方法进行安全软件的开发和验证是目前的一个趋势，同时也是EN50128中高度推荐的方法。由于联锁逻辑本身的特点，十分适合进行形式化开发和验证。使用形式化方法进行联锁系统开发和验证，可以证明系统的内在逻辑上满足既定的安全需求,在未来的市场竞争中具有很强的优势。目前国内也有几家信号厂商在不同的安全系统中使用形式化开发方法，并取得了一定的效果。

1.2 联锁系统的形式化验证流程

卡斯柯信号有限公司通过引进国外Prover公司的形式化验证方法和工具iLock，以联锁系统通用车站为测试站场，构造站场中各类信号机、道岔、区段的状态属性，依据各信号设备之间的联锁关系，自动生成站场中的所有进路。根据联锁系统需求，设计联锁通用车站的需求验证模型，对站场内所有进路在建立过程中涉及的联锁逻辑安全进行验证。

本项目是基于形式化方法对联锁系统进行证明，采用形式化高级开发语言，对联锁系统的安全需求开展通用安全需求（General Safety Specification，GSS），建立车站信号设备的对象模型（OM），开发接口文件、站场文件（.TLE文件）和布尔逻辑文件(.VTL文件)的转换器，生成形式化验证所需要的LCF/SEIF文件，使用形式化验证工具，验证联锁数据是否满足系统安全属性要求。

验证流程如图 1所示。

图1 形式化验证流程Fig.1 Flow chart of formal verification

翻译器软件Translator由卡斯柯信号有限公司进行双链开发，其中1链采用的语言是具有安全特性的函数式编程语言OCaml。

2 翻译器软件设计

联锁数据的形式化验证过程中的输入文件包含VTL文件、TLE文件和车站信息表（Excel表格，含联锁系统与外部系统的接口文件信息），这些文件需要由翻译器软件Translator来进行翻译转换，其中，VTL文件转换为SEIF文件，TLE文件转换为LCF文件，车站信息表格转换LCF文件。

翻译器软件Translator的数据处理流程如图 2所示。

图2 翻译器软件的数据处理流程Fig.2 Data process flow chart of translator software

翻译器软件按功能可分为VTL、QDZ、HDW等7大子模块，分别实现各类接口文件的翻译及输出。以其中的站场图翻译子模块为例，接口数据翻译流程说明如图 3所示。

图3 站场图数据翻译流程Fig.3 Flow chart of translation of station/yard data

3 形式化翻译器软件的OCaml实现

3.1 函数式编程语言OCaml简介

1985年，法国高等师范学院（ENS）发布了范畴论抽象机器语言（Categorical Abstract Machine Language，Caml），之后主要由法国国立计算机及自动化研究院（INRIA）负责维护。1996年，函数式编程语言（OCaml）发布了第一个版本，其在Caml的基础上支持了面向对象编程。

ML（Meta Language）语言是OCaml的祖先，设计之初的种种特性都是为了便于开发其他语言的编译器。OCaml作为继承者，在开发其他编程语言方面也是硕果累累，如形式化证明的经典工具Coq、金融量化交易软件、Microsoft的OCaml方言F#等。

OCaml是一种多范式的编程语言，可以进行命令式编程，同时OCaml也支持面向对象程序设计（Object Oriented Programming，OOP）。然而OCaml最提倡的还是函数式编程。其实现了代数类型系统、类型推导、高阶函数、尾递归、模式匹配、词法作用域、参数化模块等特性，自诞生之日起一直是主流的函数式编程语言。OCaml默认是严格求值的（也支持惰性求值），与用户的习惯接近，使程序的行为更容易预测。合理使用OCaml提供的基础设计，可以得到非常简洁有效的代码。

OCaml语言主要有如下优点。

1）Ocaml是一种功能强大的类型系统，具有参数多态性及类型推理。

2）提供用户可定义的代数数据类型和模式匹配。新的代数数据类型可以定义为记录和总和的组合，通过模式匹配（match）定义在此类数据结构上运行的函数，它提供了一种同时检查和命名数据的方式。

3）具有自动内存管理功能，这归功于一个快速、不显眼的增量垃圾回收器。

4）具有独立应用程序的单独编译功能。

综上所述，OCaml适合编写高性能、专门性强、结构复杂、正确度高、安全性好的软件，目前一般用于编译器、程序分析、金融交易、虚拟机等方面的软件开发。

3.2 输入文件参数与结构定义

TLE文件中设备的基本数据结构包含元素列表、标签名称及属性列表等，如图 4所示。

图4 TLE数据结构定义Fig.4 Definition of TLE data structure

读取TLE数据时，每类设备的结构均有所定义，如道岔、信号机、区段等，最终整体上采用哈希表来表示所采集提取到的设备集合，如图 5所示。

图5 设备结构定义Fig.5 Definition of equipment structure

3.3 翻译逻辑的OCaml实现

OCaml代码通过使用列表、哈希表，充分利用了OCaml语言的类型推断、模式匹配、参数化模块和高阶函数等特性，使程序变得非常简洁且安全可靠。

针对TLE文件，read_elem函数依次读取数据中的元素，具体实现如图 6所示。该函数中应用rec关键字来实现递归函数，同时应用match with语句来实现所有字符串的正则表达式匹配，通过“|”来实现简洁的模式匹配，如果遇到未匹配情况，会给出相应的提示信息。

图6 读取数据元素Fig.6 Read the data element

3.4 翻译结果的数据处理

翻译后的结果数据通过打包、存储等过程，存入相应的LCF文件中，用作Prover iLock软件的验证输入。

LCF文件的结构体定义如图 7所示。

图7 LCF文件结构体定义Fig.7 Definition of LCF file structure

对数据进行翻译转换，函数定义和实现如图 8所示。

图8 翻译转换函数Fig.8 Translation conversion function

打包的数据集通过emit_tables函数输出到指定文件，结果如图 9所示。

图9 翻译结果LCF文件格式与内容Fig.9 Format and content of LCF file

4 结束语

本文通过函数式编程语言OCaml开发的形式化验证翻译器软件，利用其独有的安全特性，将联锁系统的TLE、VTL等输入文件翻译为LCF/SEIF文件等，用作Prover公司形式化软件iLock的验证输入，在处理流程上保障了数据的可靠性，从而提升了联锁系统形式化验证的安全性和完备性。