實(shí)時(shí)模型檢測中精確加速的研究.pdf

1、實(shí)時(shí)系統(tǒng)經(jīng)常會出現(xiàn)不同的時(shí)間度量。然而，當(dāng)這些系統(tǒng)建模成時(shí)間自動機(jī)，然后運(yùn)用符號模型檢測技術(shù)進(jìn)行驗(yàn)證時(shí)，驗(yàn)證速度會由于不必要的符號狀態(tài)空間分裂（片段問題）而明顯下降。
　　 精確加速可以解決由于不同時(shí)間度量而造成的模型檢測時(shí)出現(xiàn)的片段問題，而且它不改變時(shí)間自動機(jī)的可達(dá)性，并可以有效地加速前向符號可達(dá)性分析。本文中，我們對精確加速原理進(jìn)行了剖析，提出了一種基于駐留環(huán)實(shí)現(xiàn)精確加速的方法，解決了原來精確加速中附加環(huán)的大小需要依賴于可加

2、速環(huán)窗口的問題，使得時(shí)間自動機(jī)精確加速模型的構(gòu)造更加的簡單快捷。同時(shí)我們還利用得出的推論，探討了一種快速計(jì)算駐留環(huán)邊界條件的方法，雖延時(shí)了加速的時(shí)機(jī)，但避免了可加速環(huán)窗口的復(fù)雜計(jì)算。
　　 此外，為了實(shí)現(xiàn)精確加速，還提出了一種識別時(shí)間自動機(jī)中可加速環(huán)的方法。針對時(shí)間自動機(jī)規(guī)模較大的問題，在識別可加速環(huán)的方法中引入拓?fù)渑判虻乃枷?，通過簡化時(shí)間自動機(jī)的規(guī)模，提高了識別時(shí)間自動機(jī)中可加速環(huán)的效率。通過實(shí)例驗(yàn)證和復(fù)雜度分析說明該方法是可