一種基于混合式監(jiān)控機制的優(yōu)化監(jiān)控開銷方法研究.pdf

1、運行時驗證是一種輕量級的形式化驗證方法，它通過檢測目標系統(tǒng)的當前執(zhí)行是否滿足給定的高層規(guī)約來實現(xiàn)對目標系統(tǒng)的驗證。對于復(fù)雜的驗證系統(tǒng)，運行時開銷有時是非常巨大的。減少運行時開銷，是運行時驗證中一個至關(guān)重要的研究內(nèi)容。因此，優(yōu)化監(jiān)控過程中的運行時開銷不僅能夠有效地緩解了監(jiān)控器生成過程中的組合爆炸問題，而且能驗證實時性和并發(fā)性的要求。
　　為了解決運行時驗證中的優(yōu)化開銷問題，本文提出了一種基于混合式監(jiān)控機制的優(yōu)化監(jiān)控開銷方法。該方法在

2、混合式監(jiān)控機制的基礎(chǔ)上，結(jié)合事件觸發(fā)監(jiān)控方式和時間觸發(fā)監(jiān)控方式的優(yōu)勢，通過數(shù)學(xué)規(guī)劃方法實現(xiàn)了開銷優(yōu)化方案的求解，從而實現(xiàn)了運行時開銷對系統(tǒng)影響最小化的目標。具體工作如下:
　　第一，對帶有關(guān)鍵指令的控制流圖進行優(yōu)化，實現(xiàn)了監(jiān)控器以一個優(yōu)化的采樣頻率來對程序進行采樣，即將運行時驗證中的優(yōu)化開銷問題轉(zhuǎn)化為帶有關(guān)鍵指令的控制流圖(CFG)優(yōu)化問題，將CFG圖轉(zhuǎn)換成整數(shù)線性規(guī)劃模型，再對模型進行求解得到最優(yōu)值，從而實現(xiàn)最優(yōu)化的CFG圖。<