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

Design of Interlocking Translator Software Oriented to Formal Verification

作　　者：王绍新 王燕芩 闫连山[3] Wang Shaoxin;Wang Yanqin;Yan Lianshan(CASCO Signal(Chengdu)Ltd.,Chengdu 610083,China;CASCO Signal Ltd.,Shanghai 200071,China;College of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756,China)

机构地区：[1]卡斯柯信号(成都)有限公司,成都610083 [2]卡斯柯信号有限公司,上海200071 [3]西南交通大学信息科学与技术学院,成都611756

出　　处：《铁路通信信号工程技术》2022年第2期18-23,42,共7页Railway Signalling & Communication Engineering

基　　金：中国国家铁路局集团有限公司科技研究开发计划重点课题(N2021S003);四川省重大科技专项(2019ZDZX0007)。

摘　　要：根据联锁系统的形式化验证系统需求,设计一种联锁数据翻译器软件的总体方案,实现站点接口文件、T LE文件和布尔逻辑文件等文件的翻译转换,生成形式化验证所需要的LCF文件。最后详细说明翻译器软件基于函数式语言OCaml的代码实现。According to the system requirements in formal verification of the interlocking system,this paper designs an overall scheme of translator software for interlocking data,which realizes the translation and conversion of station interface files,TLE files and Boolean logic files,and generates the LCF files for formal verifi cation.Finally,the code implementation of the translator software based on the functional language OCaml is explained in detail.

关 键 词：联锁系统 形式化验证 翻译器软件 OCaml 函数式语言 

分 类 号：U294.362[交通运输工程—交通运输规划与管理]