[發明專利]可編程控制器程序的安全檢查方法、裝置和設備

有效

• 申請號: 201810247212.8
• 申請日: 2018-03-23
• 公開（公告）號: CN108681503B
• 公開（公告）日: 2021-10-22
• 發明（設計）人: 鄔惠峰;張方德;嚴義
• 申請（專利權）人: 杭州電子科技大學
• 主分類號: G06F11/36
• 分類號: G06F11/36;G05B19/05
• 代理公司: 北京同立鈞成知識產權代理有限公司 11205
• 代理人: 胡艾青;劉芳

1.一種可編程控制器程序的安全檢查方法，其特征在于，包括：

根據待檢業務系統的可編程控制器PLC程序，獲得狀態轉移模型，其中，所述狀態轉移模型指示了所述待檢PLC程序運行過程中所述待檢業務系統可能出現的所有業務狀態和所有所述業務狀態之間的轉移關系；

獲取用于描述業務安全檢查規則的邏輯命題集合；

根據所述邏輯命題集合，在所述狀態轉移模型中對所有所述業務狀態進行查找，獲得不符合所述邏輯命題集合的異常業務狀態和包含所述異常業務狀態的異常轉移關系；

所述根據待檢業務系統的PLC程序，獲得狀態轉移模型，包括：

獲取所述PLC程序中各個變量的取值范圍；

根據所述各個變量的取值范圍，獲得與所述各個變量對應的賦值的集合，每個所述變量都與所述賦值的集合中至少一個賦值相對應；

以預設的初始狀態為所述PLC程序的開始狀態，根據所述賦值的集合對所述PLC程序中各個變量進行取值，獲得所述待檢業務系統可能出現的所有業務狀態、每個業務狀態對應的相關變量、每個所述相關變量的值以及所有所述業務狀態之間的轉移關系，其中，所述相關變量為所述待檢業務系統處于所述業務狀態時所述PLC程序已使用和可能要使用的變量；

將每個所述業務狀態、每個業務狀態對應的所有相關變量、每個所述相關變量的值確定為一個模型節點，將所述轉移關系確定為模型節點之間的連接關系，獲得狀態轉移模型。

2.根據權利要求1所述的方法，其特征在于，根據所述邏輯命題集合，在所述狀態轉移模型中對所有所述業務狀態進行查找，獲得不符合所述邏輯命題集合的異常業務狀態和異常轉移關系之后，還包括：

將與所述異常業務狀態對應的相關變量和每個所述相關變量的值，分別確定為異常相關變量和每個所述異常相關變量的值；

根據所述異常相關變量、每個所述異常相關變量的值以及所述異常轉移關系，在所述PLC程序中確定異常程序位置。

3.根據權利要求2所述的方法，其特征在于，在所述PLC程序中確定異常程序位置之后，還包括：

根據所述異常程序位置，獲得用于指示所述異常程序位置的錯誤報告。

4.根據權利要求1所述的方法，其特征在于，所述狀態轉移模型為計算樹邏輯模型；

相應地，所述將每個所述業務狀態、每個業務狀態對應的所有相關變量、每個所述相關變量的值確定為一個模型節點，將所述轉移關系確定為模型節點之間的連接關系，獲得狀態轉移模型，包括：

將每個所述業務狀態、每個業務狀態對應的所有相關變量、每個所述相關變量的值確定為一個模型節點，將所述轉移關系確定為模型節點之間的連接關系，獲得計算樹邏輯模型；

相應地，所述根據所述邏輯命題集合，在所述狀態轉移模型中對所有所述業務狀態進行查找，獲得不符合所述邏輯命題集合的異常業務狀態和包含異常業務狀態的異常轉移關系，包括：

根據所述邏輯命題集合，在所述計算樹邏輯模型中對所有所述業務狀態進行查找，獲得不符合所述邏輯命題集合的異常業務狀態和包含異常業務狀態的異常轉移關系。

5.根據權利要求1至4任一所述的方法，其特征在于，所述獲取用于描述業務安全檢查規則的邏輯命題集合，包括：

根據所述待檢業務系統的待檢業務，確定業務安全檢查規則；

將所述業務安全檢查規則按照時態邏輯命題公式進行形式化，獲得用于描述業務安全檢查規則的邏輯命題集合。