基于時(shí)間自動(dòng)機(jī)模型驗(yàn)證技術(shù).pdf

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

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

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