[發(fā)明專利]一種用于形式化驗證的聯鎖數據安全轉換方法及翻譯器

有效

• 申請?zhí)枺?/td>: 202110368555.1
• 申請日: 2021-04-06
• 公開（公告）號: CN113031934B
• 公開（公告）日: 2022-07-26
• 發(fā)明（設計）人: 魏民;王燕芩;張銘瑤;王紹新;楊帆;劉曉;張程;張文燕
• 申請（專利權）人: 卡斯柯信號有限公司
• 主分類號: G06F8/30
• 分類號: G06F8/30;B61L19/06
• 代理公司: 上海元好知識產權代理有限公司 31323
• 代理人: 張妍;張靜潔

1.一種用于形式化驗證的聯鎖數據安全轉換方法，其特征在于，采用不同的編程方法和編程語言開發(fā)兩個具有相同功能的翻譯器，所述翻譯器識別輸入文件中的表頭關鍵詞，根據轉換規(guī)則將每個關鍵詞所關聯的變量類型進行轉換，并將轉換后的數據重新排列，生成可以被形式化驗證工具所識別的格式文件；

所述翻譯器的輸入文件至少包含：聯鎖數據中的聯鎖信息表、設備接口信息表、站場描述數據和聯鎖布爾邏輯數據，比較兩個翻譯器的輸出文件的一致性來實現對過程失效的檢測，從而保證數據的安全轉換；

所述轉換規(guī)則為：

對于整數類型I，輸入數據是整數、空值，或NA，翻譯器將整數轉化為整數，將空值或NA轉化為null；

對于布爾類型B，輸入數據是1、0、Y、N、空值、或NA，翻譯器將1、Y轉化為true，將0、N轉化為false，將空值和NA轉化為null；

對于文本類型T，輸入數據是任意字符串、空值、或NA，翻譯器將字符串原樣輸出，空值和NA轉化為null；

對于表單類型L，輸入數據是任意字符串，翻譯器將表格中的數據用“，”隔開，對于空表格，輸出”[]”；

所述重新排列方法包含：按照輸入數據原來的順序排列，識別輸入數據中的空值或NA，改寫為null，實現重新排列。

2.如權利要求1所述的用于形式化驗證的聯鎖數據安全轉換方法，其特征在于，所述翻譯器將聯鎖信息表和設備接口信息表轉換為LCF格式文件。

3.如權利要求1所述的用于形式化驗證的聯鎖數據安全轉換方法，其特征在于，所述翻譯器將站場描述數據轉換為LCF格式文件。

4.如權利要求1所述的用于形式化驗證的聯鎖數據安全轉換方法，其特征在于，所述翻譯器將聯鎖布爾邏輯數據轉換為HLL格式文件。

5.如權利要求2所述的用于形式化驗證的聯鎖數據安全轉換方法，其特征在于，所述翻譯器將聯鎖信息表中的中文/英文標點符號、所有字符及漢字統(tǒng)一轉換為英文標點符號。

6.如權利要求2所述的用于形式化驗證的聯鎖數據安全轉換方法，其特征在于，所述翻譯器讀取聯鎖信息表中的道岔位置信息，在生成的LCF格式文件中，對道岔的定位和反位有單獨的轉換描述進行區(qū)分；

所述翻譯器讀取聯鎖信息表中的區(qū)段的侵限條件，并在生成的LCF格式文件中，有單獨的轉換描述進行區(qū)分；

所述翻譯器讀取聯鎖信息表中的敵對進路和對應的敵對進路類型，并在生成的LCF格式文件中，有單獨的轉換描述進行區(qū)分。

7.如權利要求3所述的用于形式化驗證的聯鎖數據安全轉換方法，其特征在于，所述翻譯器識別輸入數據的道岔位置信息，并在生成的LCF格式文件中，對道岔位置定位和反位、道岔為進路內道岔、防護道岔、帶動道岔應有單獨的轉換描述進行區(qū)分；

所述翻譯器識別輸入數據的區(qū)段狀態(tài)信息，并在生成的LCF格式文件中，區(qū)分進路內區(qū)段、進路外侵限區(qū)段，以及條件侵限區(qū)段的侵限條件。