US 12,468,620 B2
Interlocking data safe conversion method for formal verification and translator
Min Wei, Shanghai (CN); Yanqin Wang, Shanghai (CN); Mingyao Zhang, Shanghai (CN); Shaoxin Wang, Shanghai (CN); Fan Yang, Shanghai (CN); Xiao Lui, Shanghai (CN); Cheng Zhang, Shanghai (CN); and Wenyan Zhang, Shanghai (CN)
Assigned to CASCO SIGNAL CO., LTD., Shanghai (CN)
Appl. No. 17/792,805
Filed by CASCO SIGNAL CO., LTD., Shanghai (CN)
PCT Filed Sep. 11, 2021, PCT No. PCT/CN2021/129538
§ 371(c)(1), (2) Date Oct. 13, 2022,
PCT Pub. No. WO2022/213599, PCT Pub. Date Oct. 13, 2022.
Claims priority of application No. 202110368555.1 (CN), filed on Apr. 6, 2021.
Prior Publication US 2024/0220392 A1, Jul. 4, 2024
Int. Cl. G06F 11/3604 (2025.01); B61L 19/06 (2006.01); G06F 8/51 (2018.01)
CPC G06F 11/3608 (2013.01) [B61L 19/06 (2013.01); G06F 8/51 (2013.01); B61L 2019/065 (2013.01)] 7 Claims
OG exemplary drawing
 
1. A translator, comprising:
one or more processors; and
memory and computer program code stored in memory and running on the one or more processors, wherein the computer program code and memory are configured, when executed by the one or more processors, to cause the one or more processors to convert an input file into a format file capable of being identified by a formal verification tool,
wherein the one or more processors identifies a header keyword in the input file, and converts a variable type associated with each keyword according to a conversion rule and rearranges the converted data to generate the format file capable of being identified by the formal verification tool; and
wherein the conversion rule comprises:
with regard to an integer type I, the input data is an integer, a null value, or NA, and the one or more processors converts an integer into an integer and converts the null value and the NA into null;
with regard to a Boolean type B, the input data is 1, 0, Y, N, a null value, or NA, and the one or more processors converts 1 and Y into true, converts 0 and N into false and converts the null value and the NA into null;
with regard to a text type T, the input data is any character string, a null value, or NA, and the one or more processors outputs the character string intact and converts the null value and the NA into null; and
with regard to a form type L, the input data is any character string, and the one or more processors separates data in a form with ‘,’ and outputs ‘[ ]’ for an empty form; and
wherein the input file comprises an interlocking information table in interlocking data, a device interface information table, a station yard description data, and interlocking Boolean logic data; and
wherein the one or more processors converts the interlocking information table and the device interface information table into an LCF format file; and
wherein:
the one or more processors reads turnout position information in the interlocking information table and differentiates positioning and anti-positioning of a turnout with an independent conversion description in the generated LCF format file;
the one or more processors reads beyond limit conditions of a section in the interlocking information table and differentiates the beyond limit conditions with an independent conversion description in the generated LCF format file; and
the one or more processors reads conflicting routes in the interlocking information table and corresponding conflicting route types, and differentiates the conflicting routes and the conflicting route types with an independent conversion description in the generated LCF format file.