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

有效

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

一種用于形式化驗證的聯鎖數據安全轉換方法及翻譯器，采用不同的編程方法和編程語言開發兩個具有相同功能的翻譯器，所述翻譯器的輸入文件至少包含：聯鎖數據中的聯鎖信息表、設備接口信息表、站場描述數據和聯鎖布爾邏輯數據，比較兩個翻譯器的輸出文件的一致性來實現對過程失效的檢測，從而保證數據的安全轉換。本發明無需對每個車站進行專門的形式化開發，降低了技術成本和設計風險，安全性高，兼容性好，通用性強，應用范圍廣。

技術領域

本發明涉及一種用于形式化驗證的聯鎖數據安全轉換方法及翻譯器。

背景技術

聯鎖系統是軌道交通信號系統中保證列車行車安全的核心設備，用來實現選排進路、開放信號、扳動道岔等功能，聯鎖系統的失效可能導致列車脫軌、追尾等事故，直接影響鐵路運輸作業安全。聯鎖系統中，聯鎖數據是實現特定車站聯鎖邏輯功能的載體，聯鎖數據設計錯誤會直接導致聯鎖功能的失效。因此，通過驗證聯鎖邏輯是否滿足安全需求，即對聯鎖數據進行安全校驗和和確認，是保證聯鎖系統安全運行的必要環節。然而，由于聯鎖系統邏輯龐大復雜且功能模塊間耦合眾多，且存在各種各樣現場應用的特殊功能場景，這些因素都使得對聯鎖數據的安全驗證和確認存在很大的挑戰。對此，傳統的通過人工測試的數據驗證過程已經難以覆蓋聯鎖系統有的應用場景，存在潛在的錯誤數據通道無法被測試到，這樣的數據發布到現場將面臨潛在的安全風險。

發明內容

本發明的目的在于提供一種用于形式化驗證的聯鎖數據安全轉換方法及翻譯器，無需對每個車站進行專門的形式化開發，降低了技術成本和設計風險，安全性高，兼容性好，通用性強，應用范圍廣。

為了達到上述目的，本發明提供一種翻譯器，翻譯器將輸入文件轉換為可以被形式化驗證工具所識別的格式文件。

所述翻譯器識別輸入文件中的表頭關鍵詞，根據轉換規則將每個關鍵詞所關聯的變量類型進行轉換，并將轉換后的數據重新排列，生成可以被形式化驗證工具所識別的格式文件。

所述轉換規則為：

對于整數類型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，實現重新排列。

本發明還提供一種用于形式化驗證的聯鎖數據安全轉換方法，采用不同的編程方法和編程語言開發兩個具有相同功能的翻譯器，所述翻譯器的輸入文件至少包含：聯鎖數據中的聯鎖信息表、設備接口信息表、站場描述數據和聯鎖布爾邏輯數據，比較兩個翻譯器的輸出文件的一致性來實現對過程失效的檢測，從而保證數據的安全轉換。

所述翻譯器將聯鎖信息表和設備接口信息表轉換為LCF格式文件。

所述翻譯器將站場描述數據轉換為LCF格式文件。

所述翻譯器將聯鎖布爾邏輯數據轉換為HLL格式文件。

所述翻譯器將聯鎖信息表中的中文/英文標點符號、所有字符及漢字統一轉換為英文標點符號。

所述翻譯器讀取聯鎖信息表中的道岔位置信息，在生成的LCF格式文件中，對道岔的定位和反位有單獨的轉換描述進行區分；

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