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

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

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