[發明專利]基于重寫邏輯的并發實時程序驗證的優化處理系統及其方法

有效

• 申請號: 201110186472.7
• 申請日: 2011-07-05
• 公開（公告）號: CN102231133A
• 公開（公告）日: 2011-11-02
• 發明（設計）人: 戚正偉;管海兵;梁阿磊
• 申請（專利權）人: 上海交通大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 上海交達專利事務所 31201
• 代理人: 王毓理

1.一種基于重寫邏輯的并發實時程序驗證的優化處理系統，其特征在于，包括：程序模型模塊、性質模型模塊和重寫邏輯驗證模塊，其中：程序模型模塊與重寫邏輯驗證模塊相連接并傳輸系統的狀態轉換信息，性質模型模塊與重寫邏輯驗證模塊相連接并傳輸待驗證的系統的安全性、活性等描述信息，重寫邏輯驗證模塊與上述程序模型模塊和性質模型模塊相連接并接受系統描述與系統驗證性質的信息，然后采用重寫邏輯虛擬機進行驗證；

所述的程序模型模塊包括：狀態描述子模塊、系統描述子模塊和時間描述子模塊，其中：狀態描述子模塊與系統描述子模塊相連接并傳輸狀態信息，系統描述子模塊與時間描述相連接并傳輸信息，時間描述子模塊與程序模型主模塊相連接并傳輸經過有限抽樣的時間信息；

所述的性質模型模塊包括：線性時態邏輯子模塊、公式簡化子模塊和性質模板庫子模塊，其中：線性時態邏輯子模塊與公式簡化子模塊相連并傳輸系統通過GUI接受用戶輸入，并轉為線性時態邏輯公式的信息，公式簡化子模塊與性質模型主模塊相連接并傳輸經過狀態壓縮和公式壓縮的待驗證性質描述信息，性質模板庫子模塊與性質模型主模塊相連并傳輸常見的系統驗證模板的信息簡化用戶輸入；

所述的重寫邏輯驗證模塊包括：Kripke結構子模塊，代數模擬優化子模塊，和模型檢驗虛擬機引擎子模塊，其中：Kripke結構子模塊建立通過前端的性質模型模塊和系統模型模塊合成系統整體的Kripke結構信息并輸出到代數模擬優化子模塊，代數模擬優化子模塊接收Kripke結構信息并采用代數模擬壓縮等價狀態，將優化過的Kripke結構輸出到模型檢驗虛擬機引擎子模塊，模型檢驗虛擬機引擎子模塊采用重寫邏輯驗證系統是否符合安全性和活性等性質。

2.根據權利要求1所述的基于重寫邏輯的并發實時程序驗證的優化處理系統，其特征是，所述的系統描述子模塊采用遞歸的等式公理來描述系統的層次結構，并采用Horn子句的非一階等式公理，建立系統狀態中的各部分的成員等式邏輯規范，即系統元模型數據結構。

3.根據權利要求1所述的基于重寫邏輯的并發實時程序驗證的優化處理系統，其特征是，所述的時間描述子模塊將時間的概念形式化為一個非負實數的采用等式公理描述的時間元模型數據結構。

4.一種根據上述任一權利要求所述系統的優化處理方法，其特征在于，包括以下步驟：

第一步，程序模型模塊將系統狀態轉換為系統元模型數據結構與時間元模型數據結構，將一個不精確的并發實時程序的狀態圖轉換嚴格的形式化系統元模型與時間元模型；

第二步，性質模型模塊將待驗證性質轉換為程序正確性數據結構，即對一個并發實時程序的系統性質建立線性時態邏輯元模型的數據結構；

第三步，重寫邏輯驗證模塊在現有的Real-Time?Maude基礎上，建立Kripke結構并采用商代數模型、等式抽象、代數模擬優化方法減少狀態空間。

5.根據權利要求4所述的處理方法，其特征是，所述的第一步具體為：狀態描述子模塊針對程序中出現的各種抽象數據類型，并建立等式理論系統元模型數據結構。

6.根據權利要求4所述的處理方法，其特征是，所述的第二步具體為：根據重寫邏輯框架，程序的形式化模型建立好之后，還需要建立系統正確性的模型。

7.根據權利要求4所述的處理方法，其特征是，所述的轉換具體步驟包括：

1.1)采用成員等式邏輯規范MES(∑，E)制定出系統描述的系統元模型；

1.2)分別建立連續時間、離散時間和線性時間的等式理論：建立一個等式理論的態射，將Time作為(∑，E)的子理論；

1.3)建立(∑，E)的初始代數語義：采用商代數作為其初始代數語義，并采用模型-典范可達模型作為狀態壓縮的優化方法，將狀態空間中等價的狀態壓縮成一個狀態。

8.根據權利要求4所述的處理方法，其特征是，所述的建立線性時態邏輯元模型的數據結構具體步驟包括：

2.1)建立線性時態邏輯重寫邏輯元模型，根據用戶提供的和系統自定義的正確性性質，轉化為LTL公式的語法，并進一步采用等式公理確定其重寫語義；

2.2)采用LTL公式的高效簡化方法，采用重寫邏輯來刻畫簡化算法，并直接在引擎中內建公式優化算法；

2.3)根據常見的并發實時程序的正確性性質并采用LTL來描述，并分析整理成模板庫。

9.根據權利要求4所述的處理方法，其特征是，所述的第三步具體是指：

3.1)建立模型檢驗的Kripke結構，其中包括表達系統狀態的特殊類子，為將一步重寫關系擴展為全關系，并引入的擴展時序邏輯的標記函數；

3.2)通過時間抽樣策略將無限時間轉化為有限狀態：通過代數模擬的Theoroidal映射，采用基于stuttering模擬的抽象技術，減少狀態空間；

3.3)通過該抽象技術和成員等式邏輯的定理證明：將模型檢驗推進為證明檢驗，并針對不同的模型建立完備性和可靠性的邊界條件。