| 面向形式化验证的联锁翻译器软件设计 |
| |
| 引用本文： | 王绍新,王燕芩,闫连山.面向形式化验证的联锁翻译器软件设计[J].铁路通信信号工程技术,2022(2):18-23,42. |
| |
| 作者姓名： | 王绍新 王燕芩 闫连山 |
| |
| 作者单位： | 卡斯柯信号（成都）有限公司;卡斯柯信号有限公司;西南交通大学信息科学与技术学院 |
| |
| 基金项目： | 中国国家铁路局集团有限公司科技研究开发计划重点课题(N2021S003);四川省重大科技专项(2019ZDZX0007)。 |
| |
| 摘 要： | 根据联锁系统的形式化验证系统需求,设计一种联锁数据翻译器软件的总体方案,实现站点接口文件、TLE文件和布尔逻辑文件等文件的翻译转换,生成形式化验证所需要的LCF文件.最后详细说明翻译器软件基于函数式语言OCaml的代码实现.
|
| 关 键 词： | 联锁系统 形式化验证 翻译器软件 OCaml 函数式语言 |
Design of Interlocking Translator Software Oriented to Formal Verification |
| |
| Wang Shaoxin,Wang Yanqin,Yan Lianshan.Design of Interlocking Translator Software Oriented to Formal Verification[J].Railway Signalling & Communication Engineering,2022(2):18-23,42. |
| |
| Authors: | Wang Shaoxin Wang Yanqin Yan Lianshan |
| |
| Institution: | (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) |
| |
| Abstract: | 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. |
| |
| Keywords: | interlocking system formal verification translator software OCaml functional programming |
| 本文献已被 维普 等数据库收录！ |
