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

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

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