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

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

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

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