基于時間自動機的實時系統(tǒng)形式化建模與驗證.pdf

1、實時系統(tǒng)是一種帶有時間約束的計算機系統(tǒng)．這些系統(tǒng)的許多動作的完成是與時間相關的，即要滿足一定的時間限制。為了確保實時系統(tǒng)的正確性和可靠性，需要對其進行嚴格的分析和驗證。實時系統(tǒng)的驗證不僅要求邏輯上是正確的，而且要求時間上也是正確的。時間自動機是使用最為廣泛的實時系統(tǒng)形式化建模工具。本文在R.Alur等人提出的時間自動機的基礎上深入研究了實時系統(tǒng)建模與驗證理論及其實際應用。 本文給出時間自動機的形式化定義，研究了基于時間自動機的實

2、時系統(tǒng)建模方法，并給出了時間自動機模型的優(yōu)化方法。最后對兩個實時系統(tǒng)進行分析，利用時間自動機對它們建模。實時系統(tǒng)驗證主要驗證的問題分為安全性驗證問題和活性驗證問題，安全性驗證問題可歸結為時間自動機的可達性分析，由于模型檢測方法在對系統(tǒng)驗證時存在狀態(tài)空間爆炸問題，因此，系統(tǒng)需要一種能較好解決該問題的自動規(guī)范驗證技術。為了解決區(qū)域自動機構建過程中出現(xiàn)的狀態(tài)空間爆炸問題，我們還引用了啟發(fā)式驗證方法。本文主要研究了基于歷史等價和轉換互模擬的最小