[發明專利]一種結構化文本程序的自動化驗證方法在審
| 申請號： | 201810167496.X | 申請日： | 2018-02-28 |
| 公開（公告）號： | CN108446121A | 公開（公告）日： | 2018-08-24 |
| 發明（設計）人： | 史建琦;黃滟鴻;卜祥興;熊家文;佘慶 | 申請（專利權）人： | 華東師范大學;上海華元創信軟件有限公司 |
| 主分類號： | G06F8/41 | 分類號： | G06F8/41 |
| 代理公司： | 北京辰權知識產權代理有限公司 11619 | 代理人： | 劉廣達 |
| 地址： | 200062 上*** | 國省代碼： | 上海;31 |
| 權利要求書： | 查看更多 | 說明書： | 查看更多 |
| 摘要： | |||
| 搜索關鍵詞： | 結構化文本 驗證 圖形化 工業控制系統 抽象語法樹 變量信息 遷移系統 時態邏輯 自動化 形式化驗證 靜態分析 人力成本 構建 解析 文本 | ||
1.一種結構化文本程序的自動化驗證方法，其特征在于，包括：
分別解析結構化文本程序及規范說明文本中的規范要求，得到對應的抽象語法樹和線性時態邏輯公式；
根據所述抽象語法樹生成所述結構化文本程序的圖形化中間描述，并在所述圖形化中間描述上進行靜態分析得到所述結構化文本程序中的變量信息；
根據所述圖形化中間描述和所述變量信息構建循環遷移系統模型；
驗證所述循環遷移系統模型是否滿足所述線性時態邏輯公式。
2.根據權利要求1所述的方法，其特征在于，所述分別解析結構化文本程序及規范說明文本中的規范要求，得到對應的抽象語法樹和線性時態邏輯公式，具體包括：
解析結構化文本程序得到抽象語法樹；
解析規范說明文本中的規范要求得到對應的程序所具備的性質，根據得到的程序所具備的性質生成對應的線性時態邏輯公式。
3.根據權利要求1所述的方法，其特征在，所述根據所述抽象語法樹生成所述結構化文本程序的圖形化中間描述，并在所述圖形化中間描述上進行靜態分析得到所述結構化文本程序中的變量信息，具體為：
解析所述抽象語法樹并生成所述結構化文本程序的圖形化中間描述，在所述圖形化中間描述上進行依賴分析得到所述結構化文本程序中輸出變量的依賴集合，并對所述輸出變量進行值集分析得到輸出變量的值集。
4.根據權利要求3所述的方法，其特征在于，所述根據所述圖形化中間描述和所述變量信息構建循環遷移系統模型，具體為：根據所述圖形化中間描述、所述輸出變量的依賴集合和輸出變量的值集，構建循環遷移系統模型。
5.根據權利要求1所述的方法，其特征在于，所述驗證所述循環遷移系統模型是否滿足所述線性時態邏輯公式，具體為：遍歷所述循環遷移系統模型的狀態空間，驗證所述狀態空間中的各狀態是否滿足所述線性時態邏輯公式。
6.根據權利要求1所述的方法，其特征在于，當驗證所述循環遷移系統模型不滿足所述線性時態邏輯公式時，還包括：輸出不滿足原因。
7.一種結構化文本程序的自動化驗證設備，其特征在于，包括：
一個或多個處理器，存儲一個或多個程序的存儲裝置；
當所述一個或多個程序被所述一個或多個處理器執行時，所述一個或多個處理器實現如權利要求1～6任一所述的方法。
8.一種計算機可讀存儲介質，其上存儲有計算機程序，其特征在于，所述計算機程序被處理器執行時，實現如權利要求1～6任一所述的方法。
該專利技術資料僅供研究查看技術是否侵權等信息，商用須獲得專利權人授權。該專利全部權利屬于華東師范大學;上海華元創信軟件有限公司，未經華東師范大學;上海華元創信軟件有限公司許可，擅自商用是侵權行為。如果您想購買此專利、獲得商業授權和技術合作，請聯系【客服】
本文鏈接：http://www.szxzyx.cn/pat/books/201810167496.X/1.html，轉載請聲明來源鉆瓜專利網。
