基于時間自動機模型驗證技術(shù).pdf

1、隨著計算機科學(xué)的發(fā)展，工業(yè)界越來越重視系統(tǒng)的正確性和可靠性，這樣使得形式化的模型驗證方法得到了廣泛地應(yīng)用。通過可達性分析，模型檢測可以完成對實時系統(tǒng)的安全性和活性的驗證。它的思想是搜索描述系統(tǒng)行為的轉(zhuǎn)換系統(tǒng)，然后分析可達狀態(tài)集合，從而確定系統(tǒng)是否滿足規(guī)格說明。時間自動機是包含時間約束的有限狀態(tài)轉(zhuǎn)換系統(tǒng)，它是使用最為廣泛的形式化驗證方法之一。
　　 在理論研究部分，首先分析了時間自動機的概念，然后給出了時間自動機的一些擴展形式。實

2、時系統(tǒng)中的事件能否發(fā)生對應(yīng)著時間自動機某個狀態(tài)從初始狀態(tài)開始能否可達，因此模型驗證主要任務(wù)是狀態(tài)可達性分析。驗證需要采用了一些符號化的方法來描述狀態(tài)，文中首先對時鐘區(qū)域和時鐘帶兩種方法進行了分析，然后介紹了可達性分析的兩種主要的方法。我們重點介紹了基于二元決策圖的模型驗證方法，而使用它的前提是在時間自動機的整數(shù)語義下。詳細地解釋了如何把整數(shù)語義下的狀態(tài)和轉(zhuǎn)換關(guān)系表示成二元決策圖的形式。我們給出了在這種數(shù)據(jù)結(jié)構(gòu)下的可達性分析算法的改進，對

3、該算法進行了時間復(fù)雜度分析，并結(jié)合一個具體的驗證實例對空間復(fù)雜度進行了分析，表明改進后的算法的時間復(fù)雜度基本不變，同時又降低了可達性分析的空間復(fù)雜度。
　　 在應(yīng)用研究部分，首先是介紹了基于時間自動機的驗證工具UPPAAL，然后是結(jié)合該工具給出了模型驗證的步驟和建模的標準，最后構(gòu)造了飛機著陸控制系統(tǒng)的時間自動機模型，檢測了系統(tǒng)是否安全可靠，避免了系統(tǒng)運行時出現(xiàn)錯誤。通過使用驗證工具UPPAAL，我們可以方便地為系統(tǒng)構(gòu)造模型，有利