[發明專利]基于加權下推系統的中斷驗證方法

有效

• 申請號: 201710139115.2
• 申請日: 2017-03-09
• 公開（公告）號: CN106940659B
• 公開（公告）日: 2018-09-18
• 發明（設計）人: 黃滟鴻;郭欣;史建琦;何積豐;李昂;方徽星
• 申請（專利權）人: 華東師范大學;上海豐蕾信息科技有限公司
• 主分類號: G06F9/48
• 分類號: G06F9/48
• 代理公司: 北京辰權知識產權代理有限公司 11619
• 代理人: 郎志濤

本發明公開了一種基于加權下推系統的中斷驗證方法，首先根據程序目標代碼中指令的跳轉關系將其建模成加權下推系統，然后通過加權下推系統的可達性算法，得出所有的可達格局；最后遍歷所得的可達格局，判斷當前格局信息是否滿足需求，如果不滿足，則判斷錯誤類型，返回錯誤路徑，若遍歷完所有可達格局沒有發現錯誤，則返回正確。本發明的方法可以：將實時系統的中斷驗證與加權下推系統相結合，以形式化的方式對實時系統中斷進行驗證，提高了驗證的可靠性和魯棒性；同一個模型下同時驗證有關中斷的時序邏輯、優先級反轉、內存訪問沖突以及超時問題，具有高效性，同時也節約了成本。

技術領域

本發明屬于程序的靜態分析以及模型檢驗領域,涉及一種基于加權下推系統的中斷驗證技術。

背景技術

隨著計算機和移動互聯網的飛速發展，嵌入式實時系統被廣泛應用于各個行業：制造、醫療、交通以及通信等各個行業都與嵌入式實時系統有著密切聯系。相對于普通計算機系統，嵌入式實時系統對于可靠性有著更高的要求，特別當一個實時系統應用在關乎生命的領域時，任何不可靠因素或某些強實時任務超過規定時限，都可能引起難以預測的嚴重后果。在嵌入式實時系統中，為了使系統可以及時地與外界環境進行交互，人們引入了“中斷機制”：中斷是實時系統的一個重要部分，當出現需求時，它使得處理器可以暫時停止當前程序的執行轉而去執行處理新情況的程序。然而，中斷產生的隨機性和不確定會對系統的內存安全和時間安全等方面產生不小的隱患。而通過形式化方法的技術對中斷的相關性質進行研究驗證，不僅保證了中斷機制的正常運行，而且還能提高此類系統的安全性指標。

目前國內外對于此問題已有一些驗證方法，但是都無法用同一個方法來驗證有關中斷的重要問題，比如使用中斷時間自動機(Interrupt TimedAutomata,ITA)來描述帶有中斷的多任務系統，將實時系統轉換為中斷時間自動機，通過對ITA進行可達性分析來驗證系統是否滿足某種或某幾種性質，但是當系統過于龐大時，所轉成的中斷時間自動機會產生狀態爆炸等相關問題；通過加顏色的控制流圖,用來對中斷驅動的軟件進行靜態檢查，其主要針對棧的長度和類型以及執行時間的deadline進行分析。以及通過抽象中斷機(TheAbstract Interrupt Machine,AIM)，將程序抽象到線程一層，將同步操作看作原子操作，使用抽象中斷機來描述程序中斷處理與順序非處理代碼之前的交互，通過程序邏輯中的規范語言來判斷是否存在中斷所產生的相關問題，通過AIM可以解決共享資源訪問沖突以及中斷造成的堆棧、內存溢出等問題。

發明內容

針對以上問題，本發明的目的是提供基于加權下推系統的中斷驗證方法，將程序目標代碼轉換為加權下推系統，求出加權下推系統的可達格局，繼而根據可達格局對程序進行分析，針對求出的可達格局對時序邏輯、優先級反轉、內存訪問沖突以及超時問題進行驗證。

為實現以上目的，并解決有中斷驅動的嵌入式實時系統中存在的幾類問題，本發明采取的技術方案是：一種基于加權下推系統的中斷驗證方法，包括：

步驟1：提取需要驗證的不同任務的程序的目標代碼，將其轉換為加權下推系統；

步驟2：根據所述加權下推系統的可達性算法以及問題的需求計算出Pre加權自動機或Post加權自動機，Pre加權自動機或Post加權自動機可接受的語言作為可達格局；

步驟3：遍歷步驟2獲得的所有的可達格局，在遍歷的過程中，判斷當前格局信息是否滿足驗證需求性質，如果不滿足，判讀錯誤類型，跳轉至步驟4，若遍歷完所有格局均滿足驗證需求性質，返回正確，則跳轉至步驟5；

步驟4：根據當前格局進行回溯，找出不滿足所需驗證性質的路徑，給出該程序不滿足驗證需求性質的結果，并且給出反例路徑，算法結束；

步驟5：給出所述程序滿足驗證需求性質的結果。

優選地，所述加權下推系統包括三元組W＝(P,S,f)，其中P＝(P,Γ,Δ)為下推系統，為有界冪等半環，f：Δ→D是將下推規則映射到權重。