[發明專利]一種結構化文本程序的自動化驗證裝置

在審

• 申請號: 201810167489.X
• 申請日: 2018-02-28
• 公開（公告）號: CN108446218A
• 公開（公告）日: 2018-08-24
• 發明（設計）人: 史建琦;黃滟鴻;卜祥興;熊家文;佘慶
• 申請（專利權）人: 華東師范大學;上海華元創信軟件有限公司
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京辰權知識產權代理有限公司 11619
• 代理人: 劉廣達

本發明公開了一種結構化文本程序的自動化驗證裝置，屬于工業控制系統形式化驗證領域。所述裝置包括：解析模塊，用于分別解析結構化文本程序及規范說明文本中的規范要求，得到對應的抽象語法樹和線性時態邏輯公式；靜態分析模塊，用于根據抽象語法樹生成結構化文本程序的圖形化中間描述，并在圖形化中間描述上進行靜態分析得到結構化文本程序中的變量信息；建模模塊，用于根據圖形化中間描述和變量信息構建循環遷移系統模型；驗證模塊，用于驗證循環遷移系統模型是否滿足線性時態邏輯公式。本發明中，采用自動化驗證技術對結構化文本程序進行驗證，不僅提高了驗證效率，降低了人力成本，而且有效的提高了其對應的工業控制系統的安全性和可靠性。

技術領域

本發明涉及工業控制系統形式化驗證技術領域，尤其涉及一種結構化文本程序的自動化驗證裝置。

背景技術

隨著科技技術的不斷發展與進步，智能化越來越廣泛的走進各個領域。近年來，德國提出了“工業4.0”計劃，旨在提升制造業的智能化水平，建立具有適應性、資源效率及基因工程學的智慧工廠，其他國家也相繼提出類似的工業發展計劃，可見提高制造業自動化水平已成為未來工業發展的趨勢之一?？上攵?，將會有越來越多的工業控制系統在未來應用于不同的行業中；其中，在一些關鍵性行業，如軌道交通、航空航天等，工業控制系統的安全性和可靠性極其重要，任何微小的錯誤都可能引發重大的經濟損失，甚至是人員傷亡。因而對工業控制系統進行有效驗證及其重要，而且意義重大。

發明內容

為解決現有技術的不足，本發明提供一種結構化文本程序的自動化驗證裝置，包括：解析模塊、靜態分析模塊、建模模塊和驗證模塊；

所述解析模塊，用于分別解析結構化文本程序及規范說明文本中的規范要求，得到對應的抽象語法樹和線性時態邏輯公式；

所述靜態分析模塊，用于根據所述解析模塊得到的抽象語法樹生成所述結構化文本程序的圖形化中間描述，并在所述圖形化中間描述上進行靜態分析得到所述結構化文本程序中的變量信息；

所述建模模塊，用于根據所述靜態分析模塊得到的圖形化中間描述和變量信息構建循環遷移系統模型；

所述驗證模塊，用于驗證所述建模模塊構建的循環遷移系統模型是否滿足所述解析模塊得到的線性時態邏輯公式。

可選地，所述解析模塊包括：第一解析子模塊和第二解析子模塊；

所述第一解析子模塊，用于解析結構化文本程序得到抽象語法樹；

所述第二解換子模塊，用于解析規范說明文本中的規范要求得到對應的程序所具備的性質，根據得到的程序所具備的性質生成對應的線性時態邏輯公式。

可選地，所述靜態分析模塊包括：圖形化中間描述生成子模塊和程序變量信息收集子模塊；

所述圖形化中間描述生成子模塊，用于根據所述解析模塊得到的抽象語法樹生成所述結構化文本程序的圖形化中間描述；

所述程序變量信息收集子模塊，用于在所述圖形化中間描述生成子模塊生成的所述結構化文本程序的圖形化中間描述上進行依賴分析得到所述結構化文本程序中輸出變量的依賴集合，并對所述輸出變量進行值集分析得到所述輸出變量的值集。

可選地，所述建模模塊，具體用于：根據所述圖形化中間描述生成子模塊生成的圖形化中間描述、所述程序變量信息收集子模塊得到的輸出變量的依賴集合和輸出變量的值集，構建循環遷移系統模型。

可選地，所述驗證模塊具體用于：遍歷所述建模模塊構建的循環遷移系統模型的狀態空間，驗證所述狀態空間中的各狀態是否滿足所述解析模塊得到的線性時態邏輯公式。

可選地，所述裝置還包括：輸出模塊；

所述輸出模塊，用于當所述驗證模塊驗證所述建模模塊構建的循環遷移系統模型不滿足所述解析模塊得到的線性時態邏輯公式時，輸出不滿足原因。