基于控制結(jié)構(gòu)的模型檢測加速技術(shù)及其效益研究.pdf

1、實時系統(tǒng)是一類能夠及時處理事務(wù)或執(zhí)行計算并對外部環(huán)境做出響應(yīng)的計算機系統(tǒng)，它不僅要求系統(tǒng)計算結(jié)果是正確的，而且要求結(jié)果產(chǎn)生的時間也是正確的。在這樣的系統(tǒng)中，控制程序和外界環(huán)境經(jīng)常會使用不同的時間度量，當用時間自動機對這樣的系統(tǒng)建模，然后運用符號模型檢測技術(shù)進行驗證時，會產(chǎn)生嚴重的片段問題，造成驗證速度下降，使得模型檢測所需的時間和空間增加。
　　精確加速技術(shù)可以有效地解決實時系統(tǒng)中由于不同的時間度量而出現(xiàn)的片段問題，它的關(guān)鍵技術(shù)在

2、于向時間自動機添加了一個附加環(huán)，構(gòu)造了加速模型，有效地加速了前向符號可達性分析，并且不改變時間自動機的可達性。由于這種技術(shù)能夠有效解決片段問題，目前在模型檢測可達性分析過程中得到了廣泛應(yīng)用。雖然加速技術(shù)在不斷地發(fā)展進步，然而精確加速技術(shù)還是存在一些問題的，比如構(gòu)造附加環(huán)的大小依賴可加速環(huán)窗口，這個條件限制了精確加速在實際中的應(yīng)用。
　　本文對精確加速原理進行了分析，提出了一種基于控制結(jié)構(gòu)分析的精確加速方法。通過對時間自動機的控制結(jié)

3、構(gòu)進行靜態(tài)分析，可以計算出覆蓋狀態(tài)集，把這些狀態(tài)中的控制位置作為添加附加環(huán)的候選位置，在進行可達性分析時只存儲覆蓋狀態(tài)，這種方法在加速的同時有效減少了狀態(tài)空間。本文形式化地證明了這種方法的正確性和有效性。
　　此外，在有些情況下，添加附加環(huán)之后帶來的加速效果并不明顯，在更極端的情況下，附加環(huán)的存在甚至?xí)档万炞C速度。為了實現(xiàn)有效的精確加速，本文對基于附加環(huán)的精確加速技術(shù)進行了分析，研究了其在不同條件下的加速效果，通過分析加速過程中