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

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

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

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