基于時間自動機(jī)的實(shí)時系統(tǒng)形式化建模與驗(yàn)證.pdf

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

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