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