混雜系統(tǒng)模型驗證工具的驗證效果分析.pdf

1、混雜系統(tǒng)的形式驗證技術(shù)是利用數(shù)學(xué)分析方法對混雜系統(tǒng)的安全性進(jìn)行驗證。近十年來，模型驗證技術(shù)是形式驗證研究的主要方法。模型驗證技術(shù)是指，利用計算機強大的計算功能自動地對混雜系統(tǒng)的數(shù)學(xué)模型進(jìn)行整個狀態(tài)空間中進(jìn)行遍歷搜索，對系統(tǒng)所有可能的運行軌跡進(jìn)行收斂計算或過近似計算，以檢驗系統(tǒng)的實現(xiàn)方案是否滿足系統(tǒng)的設(shè)計要求。
　　 論文首先介紹了模型驗證的概念和特點，常用的混雜系統(tǒng)建模方法如混雜自動機、混雜Petri網(wǎng)、層次結(jié)構(gòu)和時段演算。分析

2、了可達(dá)集的兩種計算方法—前向和后向可達(dá)集算法，對可達(dá)集的過近似方法作了系統(tǒng)的闡述。最后詳細(xì)介紹了模型驗證的國內(nèi)外研究狀況和常用的模型驗證工具。
　　 針對混雜系統(tǒng)連續(xù)子系統(tǒng)和離散子系統(tǒng)相互作用的特點，研究了混雜自動機模、多面體混雜自動機和混雜I/O自動機的建模方法；對于混雜系統(tǒng)的流管道過近似問題，給出了齊諾多面體(zonotopes)的基于中心點和生成元(generators)的表達(dá)式和過近似算法，分析了該算法的保守性、封閉性、

3、集合交并處理能力以及收斂性。通過比較凸多面體過近似和齊諾多面體過近似算法的適用對象、計算方法、過近似保守性和隨維數(shù)增長的計算復(fù)雜度，對兩種算法的優(yōu)劣和特點進(jìn)行了詳細(xì)的分析。
　　 針對常壓爐加熱爐系統(tǒng)(線性混雜系統(tǒng))和汽車自適應(yīng)巡航系統(tǒng)(非線性混雜系統(tǒng))建立數(shù)學(xué)模型，抽象出驗證問題，給出ACTL驗證規(guī)范。使用PHAVer和CheckMate驗證工具分別對上述兩種系統(tǒng)建立混雜I/O自動機模型和閾值切換系統(tǒng)模型，應(yīng)用齊諾多面體流管道