[發明專利]一種實時系統的循環邊界內向分析方法

有效

• 申請號: 201410520726.8
• 申請日: 2014-09-30
• 公開（公告）號: CN104317572B
• 公開（公告）日: 2017-05-24
• 發明（設計）人: 湯恩義;鮑鐵勻;李宣東;王林章;陳鑫;潘敏學
• 申請（專利權）人: 南京大學
• 主分類號: G06F9/44
• 分類號: G06F9/44
• 代理公司: 南京瑞弘專利商標事務所(普通合伙)32249
• 代理人: 楊曉玲

技術領域

本發明涉及一種動靜態結合的實時系統的循環邊界分析方法，主要利用目標制導的符號執行技術來跟蹤循環邊界的執行條件，從而實現從內向分析的角度來估算實時系統的循環邊界，屬于計算機技術、實時系統分析交叉技術應用領域。

背景技術

循環邊界是影響實時系統實時性保障的重要因素。它是指當前系統的任意一次執行，會使循環可能達到的最大迭代次數。由于問題本身的不可判定性，對循環邊界的分析不可避免地會引入誤差。按照所引入的誤差使得分析的結果偏大還是偏小，可以將循環邊界分析方法劃分為外向分析和內向分析兩類。

已有的循環邊界分析方法均為外向分析。該類分析出于保障實時系統安全性的角度考慮，所得的分析結果是實際系統中循環邊界的高估值。這使得外向分析的結果，可以直接用于估算實時系統最壞情況下的執行時間，從而為設計實時系統提供參考依據。

在實際應用中，循環邊界外向分析方法的所得到的高估值有時會偏離實際邊界值很遠，從而造成系統硬件資源的浪費，本發明給出的內向分析方法旨在為解決這一問題提供條件。作為一種必要的補充技術，循環邊界內向分析可用于估算循環至少能夠達到的最大迭代次數。用戶結合傳統的外向分析方法和本發明提出的內向分析方法，可以明確獲得循環邊界的實際范圍與誤差情況，因此，內向分析方法的出現使得循環邊界的分析技術更為完整有效。

符號執行技術是一種利用計算機以符號推導的方式來模擬系統執行的應用技術，它最早由James King于1976年應用于系統測試領域。該技術的核心思想在于，首先將系統輸入的具體值用可以代表任意值的“符號”代替，并以此構建符號狀態在特定的平臺上進行模擬執行；然后通過收集系統各路徑上關于符號值的約束條件，來獲得各執行路徑與系統輸入符號的對應關系；最終通過求解約束條件來獲得測試用例。由于傳統符號執行方法的目的在于提高測試的覆蓋率，因而其主要的關注點在于如何使符號執行盡可能地進入系統的各條不同路徑上，而循環邊界分析僅僅關注系統中的循環部分。針對這一問題，本發明對傳統的符號執行技術進行了改進，使其符號推導的執行過程僅針對循環的最大迭代路徑，從而能高效地完成循環邊界的內向分析。

發明內容

技術問題：本發明的目的是提出一種實時系統循環邊界的內向分析方法，該方法作為傳統循環邊界外向分析方法的必要補充，能保證所求得的循環邊界估計值一定可達。

技術方案：本發明基于符號執行技術提出了一種循環邊界的內向分析方法。該方法結合靜態分析技術和動態符號執行方法，且在符號執行過程中改變搜索方式而使得執行引擎能夠快速定位到各循環的最大迭代路徑，并以此為基礎高效地獲得循環邊界的估計值，本方法包含的具體步驟為：

1-1)、使用靜態分析方法定位系統中的循環塊，并將所定位到的循環塊信息緩存，以便后續的符號執行進行進一步處理，在實現循環定位的過程中，緩存各循環塊的起始位置點、入口數、出口數、各入口和出口的位置點、循環條件的基本信息，以便后續步驟使用；

1-2)、將當前待分析的實時系統編譯到符號執行平臺，以獲得待分析系統在符號執行平臺上的字節碼，直接使用已有的符號化平臺的配套編譯工具，所生成的執行碼將用于步驟1-3)的符號執行；

1-3)、在針對循環分析定制的目標制導引擎上，對步驟1-2)所生成的字節碼完成符號執行，并在執行過程中比對由步驟1-1)所保存的循環塊信息，針對特定路徑進行符號推導，從而迅速獲得各循環塊邊界的內向分析結果。

所述步驟1-3)中的符號執行方法針對循環邊界分析的要求改變了搜索方式，從而使得執行引擎能夠快速定位到系統中各循環的最大迭代路徑；該方法具有兩個執行模式——模式a和模式b，模式a的主要作用在于建立狀態池，以獲得系統中各循環的入口符號狀態，而模式b的作用在于為已經具備條件的循環塊計算內向邊界；具體如下：

2-1)將引擎的初始模式置為模式a，構建系統的初始符號狀態；在初始的符號狀態中，系統輸入由具體變量值改成了可以代表任意值的“符號”；

2-2)以模式a對系統執行碼進行符號執行，并在執行過程中比對步驟1-1)緩存的循環塊信息，當發現當前的符號狀態到達循環入口時，將該狀態加入循環內部狀態集S留待模式b處理，而選擇另一個符號狀態執行；如果沒有其它符號狀態，則切換到模式b進行循環塊邊界分析；

2-3)切換到模式b以后，引擎會從循環內部狀態集S中任取一個狀態開始，具體分析每一個循環塊的內向邊界；這一模式的符號執行被約束在程序的各個循環塊內，通過一系列符號制導求解過程，最終獲得各個循環塊的內向邊界以及各循環塊的出口狀態；