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

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

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

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