基于時間自動機模型驗證方法優(yōu)化研究.pdf

1、實時系統(tǒng)是一種帶有時間約束的計算系統(tǒng)，這些系統(tǒng)的許多動作的完成是與時間相關(guān)的，即要滿足一定的時間限制。為了確保實時系統(tǒng)的正確性和可靠性，需要對其進行嚴格的分析和驗證。實時系統(tǒng)的驗證不僅要求邏輯上是正確的，而且要求時間上也是正確的?，F(xiàn)在網(wǎng)絡(luò)協(xié)議的復(fù)雜性日益增加。協(xié)議中的每一處錯誤和缺陷都將給網(wǎng)絡(luò)系統(tǒng)的穩(wěn)定性、可靠性等帶來巨大的危害。協(xié)議的驗證中往往也需要驗證一些時間性質(zhì)。 對實時系統(tǒng)和協(xié)議通常采用形式化的方法來進行驗證。有限自動機

2、是最為重要的一種形式描述與驗證技術(shù)，它是很多形式化方法的基礎(chǔ)。它直觀性強，可實現(xiàn)與其它形式化方法的組合和轉(zhuǎn)換。但是由于其沒有清楚的時間的概念，只能處理事件的序列，而不能準(zhǔn)確地描述事件發(fā)生的時間，因此在模型驗證上的應(yīng)用受到很大的限制。為解決這個問題，R.Alur等人提出了時間自動機模型。時間自動機在有窮自動機的基礎(chǔ)上加入了時鐘變量，通過時鐘變量和時鐘值的比較來約束狀態(tài)的轉(zhuǎn)移，因此時間自動機可以準(zhǔn)確地描述帶有時間的系統(tǒng)。 時間自動機

3、的狀態(tài)空間的大小隨著問題規(guī)模的增大呈指數(shù)級遞增。當(dāng)系統(tǒng)規(guī)模較大時，基于時間自動機的驗證就會變得非常復(fù)雜。所以需要對時間自動機的模型驗證方法進行優(yōu)化。 本文主要研究了域自動機方法、帶自動機方法以及基于歷史等價和轉(zhuǎn)換互模擬的最小化方法。文中對時鐘域及其上的操作給出了一種符號化的表示方法，從而便于域自動機在實際操作中的實現(xiàn)。本文還提出了基于狀態(tài)轉(zhuǎn)移時間關(guān)系的優(yōu)化方法。該方法通過計算狀態(tài)轉(zhuǎn)移的最早可能發(fā)生時間和最晚可能發(fā)生時間來判斷轉(zhuǎn)移