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

有效

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

技術領域

本發明涉及的是一種計算機應用技術領域的系統及方法，具體是一種基于重寫邏輯的并發實時程序驗證的優化處理系統及其方法。

背景技術

根據形式化方法的一般框架，首先需要獲得系統的形式化模型M(Model，或規范Specification)，然后建立系統的正確性(Correctness)、活性(Liveness)等判定性質(Property)。由于傳統的系統開發方法不能應付系統的日益復雜化和高可靠性的要求。例如，嵌入式軟件對實時要求比較高，對系統的性能和尺寸(footprint)比較嚴格。尤其在關鍵應用領域，對系統的可靠性、健壯性要求更高，在航空領域，甚至要求系統能夠自修正。與一般應用軟件不同，嵌入式實時并發系統一般采用低層語言編寫，功能比較單一，軟件規模不是很大，但功能的正確性比較重要，但僅靠軟件測試不可能窮舉所有的可能情況。實時并發系統同時具有離散系統和連續系統的混合特性，需要建立復雜的數學模型。

軟件模型在整個系統開發工程中占據著重要地位.使用模型可以提高開發者對整個系統的觀察深度和控制復雜度的能力，給不同的開發階段提供全局統一的視圖和指導，提高軟件質量、生產率和可靠性。建模也是進行形式化分析和驗證的基礎。形式化方法采用進程代數、Petri網、自動機、時態邏輯、模型驗證等各種數學方法，對計算機系統進行形式化建模并驗證其正確性。它起源于上世紀70年代的程序驗證；至1990，其研究領域擴展到硬件驗證；本世紀初又擴展到實時系統。隨著嵌入式系統開始興起，對并發實時程序的建模與驗證成為研究熱點。

經過對現有技術的檢索發現，從內容上看，國外對并發實時程序建模方面的專利主要集中于硬件方面，如美國專利號7,188,324“Assertion?morphing?in?functional?verification?of?integrated?circuit?design”(集成電路設計的變形功能驗證)，美國專利文獻號US2007050740“Method?and?System?for?Performing?Functional?Formal?Verification?of?Logic?Circuits”(用于邏輯電路功能驗證的方法及系統)，歐洲專利號1639507“METHOD?AND?DEVICE?FOR?THE?FORMAL?VERIFICATION?OF?A?CIRCUIT”(電路功能驗證方法及系統)等。這些專利都是建立在目前比較成熟的硬件建模理論基礎上的，這些系統的不足之處在于僅對硬件比較簡單的狀態進行驗證，無法處理并發和實時程序的分析和優化。

經過對現有技術的檢索發現，美國專利文獻號US2006282807，提出了一種“SOFTWARE?VERIFICATION”(軟件驗證)抽象求精的方法對軟件正確性進行驗證；美國專利文獻號US20050166167“System?and?Method?for?Modeling，Abstraction，and?Analysis?of?Software”(軟件建模、抽象及分析系統和方法)提出了一種采用模型檢驗對軟件進行建模和分析的方法。由于模型檢驗的方法帶來的狀態爆炸問題，如果沒有較好的狀態壓縮算法，則無法處理并發程序的驗證。

中國專利申請號200510050086.X，公布了一種“嵌入式實時操作系統的建模和代碼生成方法”，該技術得到了一種對實時操作系統可視化建模圖形工具。該方法僅僅是一種可視化的建模方法，沒有針對程序的驗證和優化。中國專利申請號200410016504.9，提出了一種“基于程序代數的硬件編譯器設計方法”，該技術基于程序代數的硬件編譯器實現。但僅僅采用程序代數的理論，對編譯器設計進行了設計，沒有涉及軟件程序的驗證和優化。從上面的討論可以看出，目前并發實時程序驗證和優化的專利主要集中在硬件方面，而且對于狀態爆炸沒有良好的處理方法，也沒有涉及到嵌入式并發實時軟件相關的程序優化。

發明內容

本發明針對現有技術存在的上述不足，提供一種基于重寫邏輯的并發實時程序驗證的優化處理系統及其方法，通過重寫邏輯驗證并發實時程序，將系統的模型和即將驗證的性質均采用代數模型進行狀態空間優化，并特別采用時間元模型能夠處理實時相關的性質，采用等價狀態壓縮和代數模擬優化以提高程序驗證效率。